diff options
| author | courant | 2002-05-02 11:37:28 +0000 |
|---|---|---|
| committer | courant | 2002-05-02 11:37:28 +0000 |
| commit | 1d08096be11d3b0a8aeed8e2b1d94f92bab7d965 (patch) | |
| tree | 8286ad058ea1535ec36624122aae76785a2de729 | |
| parent | a643f402e079080e9557d996bfa871b89be2068b (diff) | |
nettoyage code
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2663 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | tactics/tauto.ml4 | 15 |
1 files changed, 6 insertions, 9 deletions
diff --git a/tactics/tauto.ml4 b/tactics/tauto.ml4 index 3e760e5728..eea887e727 100644 --- a/tactics/tauto.ml4 +++ b/tactics/tauto.ml4 @@ -109,9 +109,6 @@ let rec tauto_intuit t_reduce t_solver ist = $t_solver ) >> -let tauto_main t_reduce ist = - tauto_intuit t_reduce <:tactic< Failtac >> ist - let unfold_not_iff = function | None -> interp <:tactic<Unfold not iff>> | Some id -> @@ -122,18 +119,18 @@ let reduction_not_iff = Tacticals.onAllClauses (fun ido -> unfold_not_iff ido) let t_reduction_not_iff = valueIn (VTactic reduction_not_iff) +let intuition_gen tac = + interp (tacticIn (tauto_intuit t_reduction_not_iff tac)) + let tauto g = - try - (interp (tacticIn (tauto_main t_reduction_not_iff))) - g + try intuition_gen <:tactic<Failtac>> g with UserError _ -> errorlabstrm "tauto" [< str "Tauto failed" >] -let intuition_gen tac = - interp (tacticIn (tauto_intuit t_reduction_not_iff tac)) +let default_intuition_tac = <:tactic< Auto with * >> let intuition args = match args with - | [] -> intuition_gen <:tactic< Auto with * >> + | [] -> intuition_gen default_intuition_tac | [ Tac(_, t)] -> intuition_gen t | _ -> assert false |