diff options
| author | sacerdot | 2001-01-30 17:44:00 +0000 |
|---|---|---|
| committer | sacerdot | 2001-01-30 17:44:00 +0000 |
| commit | 329283f014ea415b96e4c907ddf38d83fcd6b2bc (patch) | |
| tree | be8675e1e935729a5e2533fb3c8bf900157b3b83 | |
| parent | 0577c06262f89785b41f110840a1646c7981fe12 (diff) | |
Bug fixed: the case [ id : ?1 -> ?2 |- ?] was missing in tauto_main
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1290 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | tactics/tauto.ml4 | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/tactics/tauto.ml4 b/tactics/tauto.ml4 index 4546f29f7c..f181957f37 100644 --- a/tactics/tauto.ml4 +++ b/tactics/tauto.ml4 @@ -88,9 +88,13 @@ let rec tauto_main () = Cut ?2-> ?3;[Intro;Cut ?1-> ?2;[Intro;Cut ?3;[Intro;Clear id| Intros;Apply id;Assumption]|Clear id]|Intros;Apply id;Intros; Assumption];$t_tauto_main + | [id:?1 -> ?2 |- ?] -> + Cut ?1;[Intro;Cut ?2;[Clear id ; $t_tauto_main | Intro; Apply id; + Assumption ]| Clear id ; $t_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 |