diff options
| -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 |