diff options
| author | herbelin | 2003-03-31 21:18:53 +0000 |
|---|---|---|
| committer | herbelin | 2003-03-31 21:18:53 +0000 |
| commit | 00608fac2d8e217232d5f2ddd28a43971bf259b7 (patch) | |
| tree | 0bd65009594d83c85a6e3f4f5bf8a0e77e0b4fc6 /proofs/refiner.mli | |
| parent | ca29570a25be8f9b8757399f5f0b72b4a9bd5e43 (diff) | |
Ajout d'un message à FailTac
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3825 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'proofs/refiner.mli')
| -rw-r--r-- | proofs/refiner.mli | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/proofs/refiner.mli b/proofs/refiner.mli index c0d047edbf..6ea71c4db2 100644 --- a/proofs/refiner.mli +++ b/proofs/refiner.mli @@ -119,7 +119,7 @@ val tclTHENLASTn : tactic -> tactic array -> tactic val tclTHENFIRSTn : tactic -> tactic array -> tactic (* A special exception for levels for the Fail tactic *) -exception FailError of int +exception FailError of int * string val tclORELSE : tactic -> tactic -> tactic val tclREPEAT : tactic -> tactic @@ -130,7 +130,7 @@ val tclTRY : tactic -> tactic val tclTHENTRY : tactic -> tactic -> tactic val tclCOMPLETE : tactic -> tactic val tclAT_LEAST_ONCE : tactic -> tactic -val tclFAIL : int -> tactic +val tclFAIL : int -> string -> tactic val tclDO : int -> tactic -> tactic val tclPROGRESS : tactic -> tactic val tclWEAK_PROGRESS : tactic -> tactic |