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 /tactics/setoid_replace.ml | |
| 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 'tactics/setoid_replace.ml')
| -rw-r--r-- | tactics/setoid_replace.ml | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/tactics/setoid_replace.ml b/tactics/setoid_replace.ml index e397cd0cfe..e44b66bd4a 100644 --- a/tactics/setoid_replace.ml +++ b/tactics/setoid_replace.ml @@ -574,10 +574,10 @@ let res_tac c a hyp = let fin = match hyp with | None -> Auto.full_trivial | Some h -> - tclORELSE (tclTHEN (tclTRY (apply h)) (tclFAIL 0)) - (tclORELSE (tclTHEN (tclTRY (tclTHEN (apply (mkApp ((Lazy.force coq_seq_sym), [|sa.set_a; sa.set_aeq; sa.set_th|]))) (apply h))) (tclFAIL 0)) + tclORELSE (tclTHEN (tclTRY (apply h)) (tclFAIL 0 "")) + (tclORELSE (tclTHEN (tclTRY (tclTHEN (apply (mkApp ((Lazy.force coq_seq_sym), [|sa.set_a; sa.set_aeq; sa.set_th|]))) (apply h))) (tclFAIL 0 "")) Auto.full_trivial) in - tclORELSE (tclTHEN (tclTRY (apply (mkApp ((Lazy.force coq_seq_refl), [|sa.set_a; sa.set_aeq; sa.set_th;c|])))) (tclFAIL 0)) + tclORELSE (tclTHEN (tclTRY (apply (mkApp ((Lazy.force coq_seq_refl), [|sa.set_a; sa.set_aeq; sa.set_th;c|])))) (tclFAIL 0 "")) (tclORELSE assumption (tclORELSE (tclTHEN (tclTRY (apply (mkApp ((Lazy.force coq_seq_sym), [|sa.set_a; sa.set_aeq; sa.set_th|])))) assumption) fin)) |