diff options
| author |  letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2006-10-05 12:38:33 +0000 |
|---|---|---|
| committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2006-10-05 12:38:33 +0000 |
| commit | 19a8469f7accf0671bc0270c66d7725ae57f6720 (patch) | |
| tree | b4e45bacc3b0949c456dd5760ff3605a7be5fb7b /proofs/refiner.ml | |
| parent | 4524219d80c2d5ea50ca8bba819bbc14bd6b9988 (diff) | |
revision de la semantique de rewrite ... in <clause>. details dans la doc
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9211 85f007b7-540e-0410-9357-904b9bb8a0f7
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 9d5fb3151..3d65406b8 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.") |