diff options
Diffstat (limited to 'proofs/refiner.ml')
| -rw-r--r-- | proofs/refiner.ml | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/proofs/refiner.ml b/proofs/refiner.ml index 9d5fb31511..3d65406b85 100644 --- a/proofs/refiner.ml +++ b/proofs/refiner.ml @@ -540,6 +540,8 @@ let tclIFTHENSELSE=ite_gen tclTHENS let tclIFTHENSVELSE=ite_gen tclTHENSV +let tclIFTHENTRYELSEMUST tac1 tac2 gl = + tclIFTHENELSE tac1 (tclTRY tac2) tac2 gl (* Fails if a tactic did not solve the goal *) let tclCOMPLETE tac = tclTHEN tac (tclFAIL_s "Proof is not complete.") |