optcomp

Author: gares

src/coq_elpi_builtins.ml

@@ -530,12 +530,14 @@ let is_global_level env u =
     let () = UGraph.check_declared_universes (Environ.universes env) set in
     true
   with UGraph.UndeclaredLevel _ -> false
+let global_push_context_set x = Global.push_context_set ~strict:true x
 [%%else]
 let is_global_level env u =
   let set = Univ.Level.Set.singleton u in
   match UGraph.check_declared_universes (Environ.universes env) set with
   | Ok () -> true
   | Error _ -> false
+let global_push_context_set x = Global.push_context_set x
 [%%endif]
 
 let err_if_contains_alg_univ ~depth t =
@@ -2103,7 +2105,7 @@ Supported attributes:
        | Polymorphic_ind_entry uctx ->
           (Polymorphic_entry uctx, UState.Polymorphic_entry uctx, univ_binders)
        in
-     let () = Global.push_context_set uctx in
+     let () = global_push_context_set uctx in
      let mind =
        declare_mutual_inductive_with_eliminations ~primitive_expected ~default_dep_elim me (uentry', ubinders) ind_impls in
      let ind = mind, 0 in