correction bugs Tauto

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2905 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 25 insertions, 9 deletions

diff --git a/tactics/tauto.ml4 b/tactics/tauto.ml4
index a54b69360..f4f8452fa 100644
--- a/tactics/tauto.ml4
+++ b/tactics/tauto.ml4
@@ -57,7 +57,7 @@ let axioms ist =
   and t_is_empty = tacticIn is_empty in
   <:tactic<
     Match Reverse Context With
-    |[|- ?1] -> $t_is_unit;Constructor
+    |[|- ?1] -> $t_is_unit;Constructor 1
     |[_:?1 |- ?] -> $t_is_empty
     |[_:?1 |- ?1] -> Assumption>>
 
@@ -76,14 +76,28 @@ let simplif t_reduce ist =
         | [id: (?1 ? ?) |- ?] -> $t_is_disj;Elim id;Intro;Clear id;$t_reduce
         | [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;Constructor;Fail]
+          $t_is_unit;Cut ?2;
+	    [Intro;Clear id
+	    | (* id : ?1 -> ?2 |- ?2 *)
+	      Cut ?1;[Exact id|Constructor 1;Fail]
+	    ]
         | [id: (?1 ?2 ?3) -> ?4|- ?] ->
-          $t_is_conj;Cut ?2-> ?3-> ?4;[Intro;Clear id;$t_reduce|
-            Intros;Apply id;Try Split;Assumption]
+          $t_is_conj;Cut ?2-> ?3-> ?4;
+	    [Intro;Clear id;$t_reduce
+	    | (* id: (?1 ?2 ?3) -> ?4 |- ?2 -> ?3 -> ?4 *)
+	      Intro;Intro; Cut (?1 ?2 ?3);[Exact id|Split;Assumption]
+	    ]
         | [id: (?1 ?2 ?3) -> ?4|- ?] ->
-          $t_is_disj;Cut ?3-> ?4;[Cut ?2-> ?4;[Intros;Clear id;$t_reduce|
-            Intros;Apply id;
-            Try Left;Assumption]|Intros;Apply id;Try Right;Assumption]
+          $t_is_disj;
+	    Cut ?3-> ?4;
+	      [Cut ?2-> ?4;
+	        [Intro;Intro;Clear id;$t_reduce
+		| (* id: (?1 ?2 ?3) -> ?4 |- ?2 -> ?4 *)
+		  Intro; Cut (?1 ?2 ?3);[Exact id|Left;Assumption]
+		]
+	      | (* id: (?1 ?2 ?3) -> ?4 |- ?3 -> ?4 *)
+		Intro; Cut (?1 ?2 ?3);[Exact id|Right;Assumption]
+	      ]
         | [|- (?1 ? ?)] -> $t_is_conj;Split;$t_reduce);
        $t_not_dep_intros)>>
 
@@ -100,7 +114,7 @@ let rec tauto_intuit t_reduce t_solver ist =
       | [id:(?1-> ?2)-> ?3|- ?] ->
 	  Cut ?3;
 	    [Intro;Clear id
-	    |Cut ?1 -> ?2;
+	    | Cut ?1 -> ?2;
 	       [Exact id|Generalize [y:?2](id [x:?1]y);Intro;Clear id]
 	    ]; Solve [ $t_tauto_intuit ]
       | [|- (?1 ? ?)] ->
@@ -129,7 +143,9 @@ let simplif_gen = interp (tacticIn (simplif t_reduction_not_iff))
 
 let tauto g =
   try intuition_gen <:tactic<Fail>> g
-  with UserError _ -> errorlabstrm "tauto" [< str "Tauto failed" >]
+  with
+    Refiner.FailError _ | UserError _ ->
+      errorlabstrm "tauto" [< str "Tauto failed" >]
 
 let default_intuition_tac = <:tactic< Auto with * >>