Adapt to coq/coq#19620 (Global.push_context_set no strict argument)

mit-plv · Oct 15, 2024 · 848a99b · 848a99b
1 parent 76973c4
commit 848a99b
Show file tree

Hide file tree

Showing 3 changed files with 3 additions and 3 deletions.
diff --git a/src/Rewriter/Util/plugins/inductive_from_elim.ml.v819 b/src/Rewriter/Util/plugins/inductive_from_elim.ml.v819
@@ -45,7 +45,7 @@ let make_inductive_from_elim sigma (name : Names.Id.t option) (elim_ty : EConstr
     let univs, ubinders = Evd.check_univ_decl ~poly:false sigma UState.default_univ_decl in
     let uctx = match univs with
     | UState.Monomorphic_entry ctx ->
-      let () = Global.push_context_set ~strict:true ctx in
+      let () = Global.push_context_set ctx in
       Entries.Monomorphic_ind_entry
     | UState.Polymorphic_entry uctx -> Entries.Polymorphic_ind_entry uctx
     in

diff --git a/src/Rewriter/Util/plugins/inductive_from_elim.ml.v820 b/src/Rewriter/Util/plugins/inductive_from_elim.ml.v820
@@ -45,7 +45,7 @@ let make_inductive_from_elim sigma (name : Names.Id.t option) (elim_ty : EConstr
     let univs, ubinders = Evd.check_univ_decl ~poly:false sigma UState.default_univ_decl in
     let uctx = match univs with
     | UState.Monomorphic_entry ctx ->
-      let () = Global.push_context_set ~strict:true ctx in
+      let () = Global.push_context_set ctx in
       Entries.Monomorphic_ind_entry
     | UState.Polymorphic_entry uctx -> Entries.Polymorphic_ind_entry uctx
     in

diff --git a/src/Rewriter/Util/plugins/inductive_from_elim.ml.v821 b/src/Rewriter/Util/plugins/inductive_from_elim.ml.v821
@@ -45,7 +45,7 @@ let make_inductive_from_elim sigma (name : Names.Id.t option) (elim_ty : EConstr
     let univs, ubinders = Evd.check_univ_decl ~poly:false sigma UState.default_univ_decl in
     let uctx = match univs with
     | UState.Monomorphic_entry ctx ->
-      let () = Global.push_context_set ~strict:true ctx in
+      let () = Global.push_context_set ctx in
       Entries.Monomorphic_ind_entry
     | UState.Polymorphic_entry uctx -> Entries.Polymorphic_ind_entry uctx
     in