Merge PR #11723: Fix mishandling of sigma in guess_elim (regression from 8.11)

Reviewed-by: ppedrot

2 files changed, 29 insertions, 8 deletions

diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 83423b7556..ef50c56dc4 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -4246,25 +4246,26 @@ type eliminator_source =
   | ElimOver of bool * Id.t
 
 let find_induction_type isrec elim hyp0 gl =
-  let sigma, scheme,elim =
+  let sigma, indref, nparams, elim =
     match elim with
     | None ->
        let sort = Tacticals.New.elimination_sort_of_goal gl in
-       let sigma, (elimc,elimt),_ = guess_elim isrec false sort hyp0 gl in
-       let scheme = compute_elim_sig sigma ~elimc elimt in
-       (* We drop the scheme waiting to know if it is dependent *)
-       sigma, scheme, ElimOver (isrec,hyp0)
+       let sigma', (elimc,elimt),_ = guess_elim isrec false sort hyp0 gl in
+       let scheme = compute_elim_sig sigma' ~elimc elimt in
+       (* We drop the scheme and elimc/elimt waiting to know if it is dependent, this
+          needs no update to sigma at this point. *)
+       Tacmach.New.project gl, scheme.indref, scheme.nparams, ElimOver (isrec,hyp0)
     | Some e ->
         let sigma, (elimc,elimt),ind_guess = given_elim hyp0 e gl in
         let scheme = compute_elim_sig sigma ~elimc elimt in
         if Option.is_empty scheme.indarg then error "Cannot find induction type";
         let indsign = compute_scheme_signature sigma scheme hyp0 ind_guess in
         let elim = ({ elimindex = Some(-1); elimbody = elimc },elimt) in
-        sigma, scheme, ElimUsing (elim,indsign)
+        sigma, scheme.indref, scheme.nparams, ElimUsing (elim,indsign)
   in
-  match scheme.indref with
+  match indref with
   | None -> error_ind_scheme ""
-  | Some ref -> sigma, (ref, scheme.nparams, elim)
+  | Some ref -> sigma, (ref, nparams, elim)
 
 let get_elim_signature elim hyp0 gl =
   compute_elim_signature (given_elim hyp0 elim gl) hyp0
diff --git a/test-suite/bugs/closed/bug_11722.v b/test-suite/bugs/closed/bug_11722.v
new file mode 100644
index 0000000000..d4bd5f48b2
--- /dev/null
+++ b/test-suite/bugs/closed/bug_11722.v
@@ -0,0 +1,20 @@
+Require Import Program.
+Set Universe Polymorphism.
+
+Inductive paths@{i} (A : Type@{i}) (a : A) : A -> Type@{i} :=
+  idpath : paths A a a.
+
+Inductive nat :=
+  | O : nat
+  | S : nat -> nat.
+
+Axiom cheat : forall {A}, A.
+
+Program Definition foo@{i} : forall x : nat, paths@{i} nat x x := _.
+Next Obligation.
+  destruct x.
+  constructor.
+  apply cheat.
+Defined. (* FIXED: Universe unbound error *)
+
+Check foo@{_}.