From 34bd588e88312b44b44bca710651fabeefc06df2 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ga=C3=ABtan=20Gilbert?= Date: Tue, 1 Oct 2024 15:57:13 +0200 Subject: [PATCH] Adapt to coq/coq#19620 (Global.push_context_set no strict argument) --- src/principles.ml | 4 ++-- src/subterm.ml | 2 +- 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/src/principles.ml b/src/principles.ml index 4f9d93fb..018b4f80 100644 --- a/src/principles.ml +++ b/src/principles.ml @@ -1690,7 +1690,7 @@ let build_equations ~pm with_ind env evd ?(alias:alias option) rec_info progs = let univs, ubinders = Evd.univ_entry ~poly sigma 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 @@ -1759,7 +1759,7 @@ let build_equations ~pm with_ind env evd ?(alias:alias option) rec_info progs = if not poly then (* Declare the universe context necessary to typecheck the following definitions once and for all. *) - (Global.push_context_set ~strict:true (Evd.universe_context_set !evd); + (Global.push_context_set (Evd.universe_context_set !evd); evd := Evd.from_env (Global.env ())) else () in diff --git a/src/subterm.ml b/src/subterm.ml index 82927541..93cdd8a8 100644 --- a/src/subterm.ml +++ b/src/subterm.ml @@ -152,7 +152,7 @@ let derive_subterm ~pm env sigma ~poly (ind, u as indu) = let univs, ubinders = Evd.univ_entry ~poly sigma 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