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