From 50de1d310fb5a0d94fe7449f622fb5c4b751a46c Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Sun, 1 Mar 2020 13:11:20 +0100
Subject: Fix mishandling of sigma in guess_elim (regression from 8.11)

In case no eliminator is given, we wait until `get_eliminator` to
produce the actual eliminator. Using the sigma produced by guess_elim
here would insert an unused universe for the predicate's type in the
sigma.
---
 tactics/tactics.ml | 9 +++++----
 1 file changed, 5 insertions(+), 4 deletions(-)

diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 8371da76b2..dc6e18885f 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -4250,10 +4250,11 @@ let find_induction_type isrec elim hyp0 gl =
     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 waiting to know if it is dependent, this
+          needs no update to sigma at this point. *)
+       Tacmach.New.project gl, scheme, 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
-- 
cgit v1.2.3


From add9c92bed5d570d3fb4073619d8b4eb84d86848 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Sun, 1 Mar 2020 13:32:55 +0100
Subject: test-suite file for spurious universe generation

---
 test-suite/bugs/closed/bug_11722.v | 20 ++++++++++++++++++++
 1 file changed, 20 insertions(+)
 create mode 100644 test-suite/bugs/closed/bug_11722.v

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@{_}.
-- 
cgit v1.2.3


From e33bca2f54fea713822454ef4c85b801abc9709b Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Mon, 2 Mar 2020 15:01:47 +0100
Subject: Refine patch for clearer scoping of evar_map

---
 tactics/tactics.ml | 12 ++++++------
 1 file changed, 6 insertions(+), 6 deletions(-)

diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index dc6e18885f..27acc077bc 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -4246,26 +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, this
+       (* 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, ElimOver (isrec,hyp0)
+       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
-- 
cgit v1.2.3