Merge pull request #1104 from SkySkimmer/push-context-strict

Adapt to coq/coq#19620 (Global.push_context_set no strict argument)
MetaCoq · Oct 14, 2024 · fb8d911 · fb8d911
2 parents b5c0239 + f3ddc87
commit fb8d911
Show file tree

Hide file tree

Showing 2 changed files with 3 additions and 3 deletions.
diff --git a/template-coq/src/plugin_core.ml b/template-coq/src/plugin_core.ml
@@ -282,7 +282,7 @@ let tmInductive (infer_univs : bool) (mie : mutual_inductive_entry) : unit tm =
       if infer_univs then
         let evm = Evd.from_env env in
         let ctx, mie = Tm_util.RetypeMindEntry.infer_mentry_univs env evm mie in
-        Global.push_context_set ~strict:true ctx; mie
+        Global.push_context_set ctx; mie
       else mie
     in
     let names = (UState.Monomorphic_entry Univ.ContextSet.empty, UnivNames.empty_binders) in

diff --git a/template-coq/src/run_template_monad.ml b/template-coq/src/run_template_monad.ml
@@ -301,12 +301,12 @@ let declare_inductive (env: Environ.env) (evm: Evd.evar_map) (infer_univs : bool
   let mind = reduce_all env evm mind in
   let evm' = Evd.from_env env in
   let evm', ctx, mind = unquote_mutual_inductive_entry env evm' mind in
-  let () = Global.push_context_set ~strict:true ctx in
+  let () = Global.push_context_set ctx in
   let evm, mind =
     if infer_univs then
       let ctx, mind = Tm_util.RetypeMindEntry.infer_mentry_univs env evm' mind in
       debug (fun () -> Pp.(str "Declaring universe context " ++ Univ.pr_universe_context_set UnivNames.pr_level_with_global_universes ctx));
-      Global.push_context_set ~strict:true ctx;
+      Global.push_context_set ctx;
       Evd.merge_context_set Evd.UnivRigid evm ctx, mind
     else evm, mind
   in