diff options
| author | delahaye | 2001-02-05 14:27:06 +0000 |
|---|---|---|
| committer | delahaye | 2001-02-05 14:27:06 +0000 |
| commit | f54f6048ca57eeae11c62907a9089d102c8d702c (patch) | |
| tree | 2cc515d0c0cdb429505af3eb1b8367dbd79e50c9 | |
| parent | 8e42de691475823c1ed2780bd097e9ee3202244f (diff) | |
Message d'erreur plus explicite pour Tauto
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1320 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | tactics/tauto.ml4 | 22 |
1 files changed, 12 insertions, 10 deletions
diff --git a/tactics/tauto.ml4 b/tactics/tauto.ml4 index 09c7e92247..d8d3d6241c 100644 --- a/tactics/tauto.ml4 +++ b/tactics/tauto.ml4 @@ -12,6 +12,7 @@ open Proof_type open Tacmach open Tacinterp open Tactics +open Util let is_empty () = if (is_empty_type (List.assoc 1 !r_lmatch)) then @@ -91,7 +92,6 @@ let rec tauto_main () = | [|- (?1 ? ?)] -> $t_is_disj;(Left;$t_tauto_main) Orelse (Right;$t_tauto_main)>> - let intuition_main () = let t_axioms = tacticIn axioms and t_simplif = tacticIn simplif in @@ -116,17 +116,19 @@ let reduction = Tacticals.onAllClauses (fun ido -> compute ido) (* As a simple heuristic, first we try to avoid reduction both in *) (* tauto and intuition *) -let tauto = - tclTHEN (init_intros ()) - (tclORELSE - (tclTHEN reduction_not_iff (interp (tauto_main ()))) - (tclTHEN reduction (interp (tauto_main ())))) +let tauto g = + try + (tclTHEN (init_intros ()) + (tclORELSE + (tclTHEN reduction_not_iff (interp (tauto_main ()))) + (tclTHEN reduction (interp (tauto_main ()))))) g + with UserError _ -> errorlabstrm "tauto" [< 'sTR "Tauto failed" >] let intuition = - tclTHEN (init_intros ()) - (tclORELSE - (tclTHEN reduction_not_iff (interp (intuition_main ()))) - (tclTHEN reduction (interp (intuition_main ())))) + tclTHEN (init_intros ()) + (tclORELSE + (tclTHEN reduction_not_iff (interp (intuition_main ()))) + (tclTHEN reduction (interp (intuition_main ())))) let _ = hide_atomic_tactic "Tauto" tauto let _ = hide_atomic_tactic "Intuition" intuition |