From 4ec5bed75004a180595eb69c751a1af5b75c0d8d Mon Sep 17 00:00:00 2001
From: corbinea
Date: Mon, 27 Sep 2004 14:55:34 +0000
Subject: firstorder bugfix to cope with elim of sigma types with goal is of
 the wrong sort

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6141 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 contrib/first-order/ground.ml |  3 ++-
 contrib/first-order/rules.ml  | 14 ++++++++------
 contrib/first-order/rules.mli |  2 +-
 3 files changed, 11 insertions(+), 8 deletions(-)

diff --git a/contrib/first-order/ground.ml b/contrib/first-order/ground.ml
index bd155fd511..418e6ce831 100644
--- a/contrib/first-order/ground.ml
+++ b/contrib/first-order/ground.ml
@@ -117,7 +117,8 @@ let ground_tac solver startseq gl=
 			      backtrack2 (* need special backtracking *)
   		      | Lexists ind ->
 			  if !qflag then 
-			    left_exists_tac ind hd.id continue (re_add seq1)
+			    left_exists_tac ind backtrack hd.id
+			      continue (re_add seq1)
 			  else backtrack
 		      | LA (typ,lap)->
 			  let la_tac=
diff --git a/contrib/first-order/rules.ml b/contrib/first-order/rules.ml
index 82594681b3..3474fe00c3 100644
--- a/contrib/first-order/rules.ml
+++ b/contrib/first-order/rules.ml
@@ -172,13 +172,15 @@ let forall_tac backtrack continue seq=
      else
        backtrack)
 
-let left_exists_tac ind id continue seq gls=
+let left_exists_tac ind backtrack id continue seq gls=
   let n=(construct_nhyps ind gls).(0) in  
-    tclTHENLIST
-      [simplest_elim (constr_of_reference id);
-       clear_global id;
-       tclDO n intro;
-       (wrap (n-1) false continue seq)] gls
+    tclIFTHENELSE
+      (simplest_elim (constr_of_reference id))
+      (tclTHENLIST [clear_global id;
+                    tclDO n intro;
+                    (wrap (n-1) false continue seq)]) 
+      backtrack 
+      gls
 	
 let ll_forall_tac prod backtrack id continue seq=
   tclORELSE
diff --git a/contrib/first-order/rules.mli b/contrib/first-order/rules.mli
index 074b7a9f30..1c2c93a49b 100644
--- a/contrib/first-order/rules.mli
+++ b/contrib/first-order/rules.mli
@@ -47,7 +47,7 @@ val ll_arrow_tac : constr -> constr -> constr -> lseqtac with_backtracking
 
 val forall_tac : seqtac with_backtracking
 
-val left_exists_tac : inductive -> lseqtac
+val left_exists_tac : inductive -> lseqtac with_backtracking
 
 val ll_forall_tac : types -> lseqtac with_backtracking 
 
-- 
cgit v1.2.3