Adapt to coq/coq#17836 (sort poly)

mit-plv · Sep 22, 2023 · 52a910f · 52a910f
1 parent 43447bc
commit 52a910f
Show file tree

Hide file tree

Showing 3 changed files with 4 additions and 4 deletions.
diff --git a/src/Rewriter/Util/Tactics2/Constr.v.v819 b/src/Rewriter/Util/Tactics2/Constr.v.v819
@@ -53,7 +53,7 @@ Module Unsafe.
          Case.iter_invert f iv;
          f x;
          f y
-    | Proj _p c => f c
+    | Proj _p _ c => f c
     | Fix _ _ tl bl =>
         Array.iter (fun b => f (Binder.type b)) tl;
         Array.iter f bl
@@ -84,7 +84,7 @@ Module Unsafe.
          Case.iter_invert (f n) iv;
          f n x;
          f n y
-    | Proj _p c => f n c
+    | Proj _p _ c => f n c
     | Fix _ _ tl bl =>
         Array.iter (fun b => f n (Binder.type b)) tl;
         Array.iter (f (iterate g (Array.length tl) n)) bl

diff --git a/src/Rewriter/Util/Tactics2/DestProj.v.v819 b/src/Rewriter/Util/Tactics2/DestProj.v.v819
@@ -6,6 +6,6 @@ Ltac2 Type exn ::= [ Not_a_proj (kind) ].
 Ltac2 destProj (c : constr) :=
   let k := kind c in
   match k with
-  | Proj p v => (p, v)
+  | Proj p r v => (p, r, v)
   | _ => Control.throw (Not_a_proj k)
   end.
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 () = DeclareUctx.declare_universe_context ~poly:false 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