Nouveau choix pour l'intros initial

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

3 files changed, 21 insertions, 7 deletions

diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 3b152c27c..c71abe264 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -356,16 +356,22 @@ let rec intros_until s g =
 	    [<'sTR "No such hypothesis in current goal";
 	      'sTR " even after head-reduction" >]
 
-let rec intros_until_n n g =
+let rec intros_until_n_gen red n g =
   match pf_lookup_index_as_renamed (pf_concl g) n with
     | Some depth -> tclDO depth intro g
     | None ->
+      if red then
 	try
-	  ((tclTHEN (reduce (Red true) []) (intros_until_n n)) g)
+          ((tclTHEN (reduce (Red true) []) (intros_until_n_gen red n)) g)
 	with Redelimination ->
           errorlabstrm "Intros" 
 	    [<'sTR "No such hypothesis in current goal";
 	      'sTR " even after head-reduction" >]
+      else
+        errorlabstrm "Intros" [<'sTR "No such hypothesis in current goal" >]
+
+let intros_until_n = intros_until_n_gen true
+let intros_until_n_wored = intros_until_n_gen false
 
 let dyn_intros_until = function 
   | [Identifier id] -> intros_until id
diff --git a/tactics/tactics.mli b/tactics/tactics.mli
index b41c07ec3..ada02fcf2 100644
--- a/tactics/tactics.mli
+++ b/tactics/tactics.mli
@@ -77,6 +77,7 @@ val dyn_intros_using : tactic_arg list -> tactic
 i*)
 
 val intros_until         : identifier -> tactic
+val intros_until_n_wored : int -> tactic
 val dyn_intros_until     : tactic_arg list -> tactic
 
 val intros_clearing      : bool list -> tactic
diff --git a/tactics/tauto.ml4 b/tactics/tauto.ml4
index 64f6a48c8..dc8732df0 100644
--- a/tactics/tauto.ml4
+++ b/tactics/tauto.ml4
@@ -11,6 +11,7 @@ open Pp
 open Proof_type
 open Tacmach
 open Tacinterp
+open Tactics
 
 let is_empty () =
   if (is_empty_type (List.assoc 1 !r_lmatch)) then
@@ -28,13 +29,13 @@ let is_conj () =
   if (is_conjunction (List.assoc 1 !r_lmatch)) then
      <:tactic<Idtac>>
   else
-    failwith "is_conj";;
+    failwith "is_conj"
 
 let is_disj () =
   if (is_disjunction (List.assoc 1 !r_lmatch)) then
      <:tactic<Idtac>>
   else
-    failwith "is_disj";;
+    failwith "is_disj"
 
 let not_dep_intros () =
   <:tactic<
@@ -42,6 +43,10 @@ let not_dep_intros () =
       Match Context With
       | [|- ?1 -> ?2 ] -> Intro>>
 
+let init_intros () =
+  (tclORELSE (tclTHEN (intros_until_n_wored 1) (interp (not_dep_intros ())))
+    intros)
+
 let axioms () =
   let t_is_unit = tacticIn is_unit
   and t_is_empty = tacticIn is_empty in
@@ -67,7 +72,7 @@ let simplif () =
         | [id: (?1 ?2 ?3) -> ?4|- ?] ->
           $t_is_disj;Cut ?3-> ?4;[Cut ?2-> ?4;[Intros;Clear id|Intro;Apply id;
             Left;Assumption]|Intro;Apply id;Right;Assumption]
-        | [id0: ?1-> ?; id1: ?1|- ?] -> Generalize (id0 id1);Intro;Clear id0
+        | [id0: ?1-> ?2; id1: ?1|- ?] -> Generalize (id0 id1);Intro;Clear id0
         | [|- (?1 ? ?)] -> $t_is_conj;Split);$t_not_dep_intros)>>
 
 let rec tauto_main () =
@@ -100,10 +105,12 @@ let compute = function
 let reduction = Tacticals.onAllClauses (fun ido -> compute ido)
 
 let tauto =
-  (tclTHEN reduction (interp (tauto_main ())))
+  (tclTHEN (init_intros ())
+    (tclTHEN reduction (interp (tauto_main ()))))
 
 let intuition =
-  (tclTHEN reduction (interp (intuition_main ())))
+  (tclTHEN (init_intros ())
+    (tclTHEN reduction (interp (intuition_main ()))))
 
 let _ = hide_atomic_tactic "Tauto" tauto
 let _ = hide_atomic_tactic "Intuition" intuition