diff options
| author | herbelin | 2001-12-19 12:22:12 +0000 |
|---|---|---|
| committer | herbelin | 2001-12-19 12:22:12 +0000 |
| commit | a6efb365f21eb1d3def5ab7b07efe2a817cff3c1 (patch) | |
| tree | e029d3120eb11f83b980d70f057ae39c5388a63c | |
| parent | c55728a42a8de6ce47bcb07d87050da5e5fc38f9 (diff) | |
Tentative d'amélioration du résultat de Intuition
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2340 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | tactics/tauto.ml4 | 12 |
1 files changed, 9 insertions, 3 deletions
diff --git a/tactics/tauto.ml4 b/tactics/tauto.ml4 index f8ad93280e..a26f234013 100644 --- a/tactics/tauto.ml4 +++ b/tactics/tauto.ml4 @@ -126,7 +126,13 @@ let compute = function let ast_id = nvar id in interp <:tactic<Compute in $ast_id>> -let reduction = Tacticals.onAllClauses (fun ido -> compute ido) +let red = function + | None -> interp <:tactic<Repeat Red>> + | Some id -> + let ast_id = nvar id in + interp <:tactic<Repeat Red in $ast_id>> + +let reduction = Tacticals.onAllClauses (* As a simple heuristic, first we try to avoid reduction both in tauto and intuition *) @@ -136,14 +142,14 @@ let tauto g = (tclTHEN init_intros (tclORELSE (tclTHEN reduction_not_iff (interp (tacticIn tauto_main))) - (tclTHEN reduction (interp (tacticIn tauto_main))))) g + (tclTHEN (reduction compute) (interp (tacticIn tauto_main))))) g with UserError _ -> errorlabstrm "tauto" [< str "Tauto failed" >] let intuition = tclTHEN init_intros (tclORELSE (tclTHEN reduction_not_iff (interp (tacticIn intuition_main))) - (tclTHEN reduction (interp (tacticIn intuition_main)))) + (tclTHEN (reduction red) (interp (tacticIn intuition_main)))) let _ = hide_atomic_tactic "Tauto" tauto let _ = hide_atomic_tactic "Intuition" intuition |