diff options
| author | corbinea | 2003-06-22 10:58:36 +0000 |
|---|---|---|
| committer | corbinea | 2003-06-22 10:58:36 +0000 |
| commit | fc7d61f85f1e0700d75513b9b0015992e33370ec (patch) | |
| tree | 89cfa3b9f1778781a08f68d290619ffa60ea7b72 | |
| parent | 902141f7baa8ff4a480a2bfe41e2c103ef679633 (diff) | |
Ground update
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4196 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | contrib/first-order/rules.ml | 10 |
1 files 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 |