diff options
| author | courant | 2001-08-08 14:26:24 +0000 |
|---|---|---|
| committer | courant | 2001-08-08 14:26:24 +0000 |
| commit | 3ffbeb47814baf086c791da24d36efb9d88a1ab0 (patch) | |
| tree | 02096b0131485941cdba3daae9e15c0fcf3d6330 | |
| parent | d0231fa8e99ee7edd62535a0c194ab656eaba213 (diff) | |
Modification Tauto pour qu'il puisse destructurer des hypotheses de la forme
e1 -> e2 avec e1 type inductif ayant un unique constructeur constant.
Cas typique : hypothese de la forme ~e=e.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1884 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | tactics/tauto.ml4 | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/tactics/tauto.ml4 b/tactics/tauto.ml4 index acc978affd..7edf1610e5 100644 --- a/tactics/tauto.ml4 +++ b/tactics/tauto.ml4 @@ -83,7 +83,7 @@ let simplif () = Try Left;Assumption]|Intros;Apply id;Try Right;Assumption] | [id0: ?1-> ?2; id1: ?1|- ?] -> Generalize (id0 id1);Intro;Clear id0 | [id: ?1 -> ?2|- ?] -> - $t_is_unit;Cut ?2;[Intro;Clear id|Intros;Apply (id I);Assumption] + $t_is_unit;Cut ?2;[Intro;Clear id|Intros;Apply id;Constructor;Fail] | [|- (?1 ? ?)] -> $t_is_conj;Split);$t_not_dep_intros)>> let rec tauto_main () = |