From 848a99b2ca22e8d6ff01d13ff2e188641f157c0f Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ga=C3=ABtan=20Gilbert?= Date: Tue, 1 Oct 2024 16:02:37 +0200 Subject: [PATCH 1/2] Adapt to coq/coq#19620 (Global.push_context_set no strict argument) --- src/Rewriter/Util/plugins/inductive_from_elim.ml.v819 | 2 +- src/Rewriter/Util/plugins/inductive_from_elim.ml.v820 | 2 +- src/Rewriter/Util/plugins/inductive_from_elim.ml.v821 | 2 +- 3 files changed, 3 insertions(+), 3 deletions(-) diff --git a/src/Rewriter/Util/plugins/inductive_from_elim.ml.v819 b/src/Rewriter/Util/plugins/inductive_from_elim.ml.v819 index 04bca0923..7f1c34db5 100644 --- 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 index 04bca0923..7f1c34db5 100644 --- 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 index 1039f9266..1e498a055 100644 --- 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 From 5bb09ecaa2f9aa4fffb49ea740d01614a5217ad9 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Tue, 15 Oct 2024 02:34:53 -0700 Subject: [PATCH 2/2] Revert changes to older code --- src/Rewriter/Util/plugins/inductive_from_elim.ml.v819 | 2 +- src/Rewriter/Util/plugins/inductive_from_elim.ml.v820 | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/src/Rewriter/Util/plugins/inductive_from_elim.ml.v819 b/src/Rewriter/Util/plugins/inductive_from_elim.ml.v819 index 7f1c34db5..04bca0923 100644 --- 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 ctx in + let () = Global.push_context_set ~strict:true 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 index 7f1c34db5..04bca0923 100644 --- 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 ctx in + let () = Global.push_context_set ~strict:true ctx in Entries.Monomorphic_ind_entry | UState.Polymorphic_entry uctx -> Entries.Polymorphic_ind_entry uctx in