From fc7d61f85f1e0700d75513b9b0015992e33370ec Mon Sep 17 00:00:00 2001
From: corbinea
Date: Sun, 22 Jun 2003 10:58:36 +0000
Subject: Ground update

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4196 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 contrib/first-order/rules.ml | 10 ++++++----
 1 file changed, 6 insertions(+), 4 deletions(-)

diff --git a/contrib/first-order/rules.ml b/contrib/first-order/rules.ml
index 74ac19614c..ad36bc4d70 100644
--- a/contrib/first-order/rules.ml
+++ b/contrib/first-order/rules.ml
@@ -83,8 +83,9 @@ let or_tac backtrack 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))
+    (tclORELSE
+       (tclTHEN introf (tclCOMPLETE (wrap 1 true continue seq)))
+       backtrack)
 (* left connectives rules *)
 
 let left_and_tac ind backtrack id continue seq=
@@ -162,8 +163,9 @@ let ll_arrow_tac a b c backtrack id continue seq=
 let forall_tac backtrack continue seq=
   tclORELSE
     (tclIFTHENELSE intro (wrap 0 true continue seq)
-       (tclTHEN introf 
-	  (tclORELSE (tclCOMPLETE (wrap 1 true continue seq)) backtrack)))
+       (tclORELSE
+	  (tclTHEN introf (tclCOMPLETE (wrap 0 true continue seq)))
+	  backtrack))
     (if !qflag then 
        tclFAIL 0 "reversible in 1st order mode"
      else
-- 
cgit v1.2.3