Ground update

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4193 85f007b7-540e-0410-9357-904b9bb8a0f7

3 files changed, 20 insertions, 17 deletions

diff --git a/contrib/first-order/ground.ml b/contrib/first-order/ground.ml
index 7571da2de..d46a4a529 100644
--- a/contrib/first-order/ground.ml
+++ b/contrib/first-order/ground.ml
@@ -42,7 +42,7 @@ let ground_tac solver startseq gl=
 			      backtrack in
 			    forall_tac backtrack continue (re_add seq1)
 		      | Rarrow->
-			  arrow_tac continue (re_add seq1)
+			  arrow_tac backtrack continue (re_add seq1)
 		      | Ror->
 			  or_tac  backtrack continue (re_add seq1)
 		      | Rfalse->backtrack 
diff --git a/contrib/first-order/rules.ml b/contrib/first-order/rules.ml
index 12593de70..74ac19614 100644
--- a/contrib/first-order/rules.ml
+++ b/contrib/first-order/rules.ml
@@ -67,7 +67,7 @@ let ll_atom_tac a backtrack id continue seq=
 	[generalize [mkApp(constr_of_reference id,
 			   [|constr_of_reference (find_left a seq)|])];
 	 clear_global id;
-	 introf]
+	 intro]
     with Not_found->tclFAIL 0 "No link") 
     (wrap 1 false continue seq) backtrack 
 
@@ -78,12 +78,13 @@ let and_tac backtrack continue seq=
 
 let or_tac backtrack continue seq=
   tclORELSE 
-    (any_constructor (Some (tclSOLVE [wrap 0 true continue seq])))
+    (any_constructor (Some (tclCOMPLETE (wrap 0 true continue seq))))
     backtrack
 
-let arrow_tac continue seq=
-  tclTHEN introf (wrap 1 true continue seq)
-   
+let arrow_tac backtrack continue seq=
+  tclIFTHENELSE intro (wrap 1 true continue seq)
+    (tclTHEN introf 
+       (tclORELSE (tclCOMPLETE (wrap 1 true continue seq)) backtrack))
 (* left connectives rules *)
 
 let left_and_tac ind backtrack id continue seq=
@@ -92,7 +93,7 @@ let left_and_tac ind backtrack id continue seq=
      (tclTHENLIST 
       [simplest_elim (constr_of_reference id);
        clear_global id; 
-       tclDO n introf])
+       tclDO n intro])
      (wrap n false continue seq)
      backtrack
 
@@ -101,7 +102,7 @@ let left_or_tac ind backtrack id continue seq=
   let f n=
     tclTHENLIST
       [clear_global id;
-       tclDO n introf;
+       tclDO n intro;
        wrap n false continue seq] in
     tclIFTHENSVELSE
       (simplest_elim (constr_of_reference id))
@@ -133,7 +134,7 @@ let ll_ind_tac ind largs backtrack id continue seq gl=
 	   (tclTHENLIST 
 	      [generalize newhyps;
 	       clear_global id;
-	       tclDO lp introf])
+	       tclDO lp intro])
 	   (wrap lp false continue seq) backtrack gl
 
 let ll_arrow_tac a b c backtrack id continue seq=
@@ -153,14 +154,16 @@ let ll_arrow_tac a b c backtrack id continue seq=
 	       [generalize [d];
 		introf;
 		clear_global id;
-		tclSOLVE [wrap 1 true continue seq]]]])
+		tclCOMPLETE (wrap 1 true continue seq)]]])
       backtrack
 
 (* quantifier rules (easy side) *)
 
 let forall_tac backtrack continue seq=
   tclORELSE
-    (tclTHEN introf (wrap 0 true continue seq))
+    (tclIFTHENELSE intro (wrap 0 true continue seq)
+       (tclTHEN introf 
+	  (tclORELSE (tclCOMPLETE (wrap 1 true continue seq)) backtrack)))
     (if !qflag then 
        tclFAIL 0 "reversible in 1st order mode"
      else
@@ -171,22 +174,22 @@ let left_exists_tac ind id continue seq=
     tclTHENLIST
       [simplest_elim (constr_of_reference id);
        clear_global id;
-       tclDO n introf;
+       tclDO n intro;
        (wrap (n-1) false continue seq)]
 	
 let ll_forall_tac prod backtrack id continue seq=
   tclORELSE
     (tclTHENS (cut prod)
        [tclTHENLIST
-	  [introf;
+	  [intro;
 	   (fun gls->
 	      let id0=pf_nth_hyp_id gls 1 in
 	      let term=mkApp((constr_of_reference id),[|mkVar(id0)|]) in
 		tclTHEN (generalize [term]) (clear [id0]) gls);  
 	   clear_global id;
-	   introf;
-	   tclSOLVE [wrap 1 false continue (deepen seq)]];
-	tclSOLVE [wrap 0 true continue (deepen seq)]])
+	   intro;
+	   tclCOMPLETE (wrap 1 false continue (deepen seq))];
+	tclCOMPLETE (wrap 0 true continue (deepen seq))])
     backtrack
 
 (* rules for instantiation with unification moved to instances.ml *)
diff --git a/contrib/first-order/rules.mli b/contrib/first-order/rules.mli
index c5c15fdd5..60756127a 100644
--- a/contrib/first-order/rules.mli
+++ b/contrib/first-order/rules.mli
@@ -33,7 +33,7 @@ val and_tac : seqtac with_backtracking
 
 val or_tac : seqtac with_backtracking
 
-val arrow_tac : seqtac
+val arrow_tac : seqtac with_backtracking
 
 val left_and_tac : inductive -> lseqtac with_backtracking