diff options
| author | letouzey | 2006-10-05 12:38:33 +0000 |
|---|---|---|
| committer | letouzey | 2006-10-05 12:38:33 +0000 |
| commit | 19a8469f7accf0671bc0270c66d7725ae57f6720 (patch) | |
| tree | b4e45bacc3b0949c456dd5760ff3605a7be5fb7b /proofs | |
| 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')
| -rw-r--r-- | proofs/refiner.ml | 2 | ||||
| -rw-r--r-- | proofs/refiner.mli | 6 |
2 files changed, 8 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.") diff --git a/proofs/refiner.mli b/proofs/refiner.mli index 72afde93e0..0225e6443e 100644 --- a/proofs/refiner.mli +++ b/proofs/refiner.mli @@ -144,6 +144,12 @@ val tclIFTHENELSE : tactic -> tactic -> tactic -> tactic val tclIFTHENSELSE : tactic -> tactic list -> tactic ->tactic val tclIFTHENSVELSE : tactic -> tactic array -> tactic ->tactic +(* [tclIFTHENTRYELSEMUST tac1 tac2 gls] applies [tac1] then [tac2]. If [tac1] + has been successful, then [tac2] may fail. Otherwise, [tac2] must succeed. + Equivalent to [(tac1;try tac2)||tac2] *) + +val tclIFTHENTRYELSEMUST : tactic -> tactic -> tactic + (*s Tactics handling a list of goals. *) type validation_list = proof_tree list -> proof_tree list |