From 35f46eabfb0f079ccfb685a1a4486ecb27b77524 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Ga=C3=ABtan=20Gilbert?= <gaetan.gilbert@skyskimmer.net>
Date: Mon, 18 Sep 2023 13:03:14 +0200
Subject: [PATCH] Adapt to coq/coq#17836 (sort poly)

---
 src/Rewriter/Util/Tactics2/Constr.v.v818              | 2 +-
 src/Rewriter/Util/Tactics2/Constr.v.v819              | 4 ++--
 src/Rewriter/Util/Tactics2/DestProj.v.v818            | 2 +-
 src/Rewriter/Util/Tactics2/DestProj.v.v819            | 2 +-
 src/Rewriter/Util/Tactics2/Proj.v.v816                | 3 +--
 src/Rewriter/Util/plugins/inductive_from_elim.ml.v819 | 2 +-
 6 files changed, 7 insertions(+), 8 deletions(-)

diff --git a/src/Rewriter/Util/Tactics2/Constr.v.v818 b/src/Rewriter/Util/Tactics2/Constr.v.v818
index 80159e377..5e4f988f4 100644
--- a/src/Rewriter/Util/Tactics2/Constr.v.v818
+++ b/src/Rewriter/Util/Tactics2/Constr.v.v818
@@ -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 _r 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/Constr.v.v819 b/src/Rewriter/Util/Tactics2/Constr.v.v819
index 80159e377..56f214813 100644
--- 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.v818 b/src/Rewriter/Util/Tactics2/DestProj.v.v818
index 552f88ca0..3e8181f91 100644
--- a/src/Rewriter/Util/Tactics2/DestProj.v.v818
+++ b/src/Rewriter/Util/Tactics2/DestProj.v.v818
@@ -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/Tactics2/DestProj.v.v819 b/src/Rewriter/Util/Tactics2/DestProj.v.v819
index 552f88ca0..3e8181f91 100644
--- 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/Tactics2/Proj.v.v816 b/src/Rewriter/Util/Tactics2/Proj.v.v816
index 6c0e12e9c..61730b129 100644
--- a/src/Rewriter/Util/Tactics2/Proj.v.v816
+++ b/src/Rewriter/Util/Tactics2/Proj.v.v816
@@ -4,5 +4,4 @@ Import Ltac2.Constr.
 Import Constr.Unsafe.
 
 Ltac2 equal (x : projection) (y : projection) : bool
-  := let dummy := make (Rel (-1)) in
-     Constr.equal (make (Proj x dummy)) (make (Proj y dummy)).
+  := Proj.equal x y.
diff --git a/src/Rewriter/Util/plugins/inductive_from_elim.ml.v819 b/src/Rewriter/Util/plugins/inductive_from_elim.ml.v819
index 9a31cfa14..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 () = 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