From c938cb8e85f741ce697e7486d35c27c1aa31fe7a Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Wed, 10 Dec 2014 18:17:39 +0100
Subject: Fix dummy argument use in guess_elim: there are some cases where
 X_ind is not defined while X_rect is, for example in HoTT/Coq.

---
 tactics/tactics.ml | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 63afd3a5b0..3a0baf2946 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -3583,7 +3583,9 @@ let find_induction_type isrec elim hyp0 gl =
   let scheme,elim =
     match elim with
     | None ->
-	let _, (elimc,elimt),_ = guess_elim isrec (* dummy: *) true (* dummy: *) InProp hyp0 gl in
+       let sort = Tacticals.New.elimination_sort_of_goal gl in
+       let _, (elimc,elimt),_ = 
+	 guess_elim isrec (* dummy: *) true sort hyp0 gl in
 	let scheme = compute_elim_sig ~elimc elimt in
 	(* We drop the scheme waiting to know if it is dependent *)
 	scheme, ElimOver (isrec,hyp0)
-- 
cgit v1.2.3