Add the option to automatically introduce variables declared before the

colon in (mutual) proofs with [Set Automatic Introduction].
Fix a minor test-suite issue in ProgramWf due to new handling of the
default obligation tactic.


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

6 files changed, 49 insertions, 10 deletions

diff --git a/lib/flags.ml b/lib/flags.ml
index 1bf393fd0..da8013028 100644
--- a/lib/flags.ml
+++ b/lib/flags.ml
@@ -55,6 +55,10 @@ let verbosely f x = without_option silent f x
 let if_silent f x = if !silent then f x
 let if_verbose f x = if not !silent then f x
 
+let auto_intros = ref false
+let make_auto_intros flag = auto_intros := flag
+let is_auto_intros () = !auto_intros
+
 let hash_cons_proofs = ref true
 
 let warn = ref true
diff --git a/lib/flags.mli b/lib/flags.mli
index 8bafa8b1f..e8a7819c8 100644
--- a/lib/flags.mli
+++ b/lib/flags.mli
@@ -42,6 +42,9 @@ val verbosely : ('a -> 'b) -> 'a -> 'b
 val if_silent : ('a -> unit) -> 'a -> unit
 val if_verbose : ('a -> unit) -> 'a -> unit
 
+val make_auto_intros : bool -> unit
+val is_auto_intros : unit -> bool
+
 val make_warn : bool -> unit
 val if_warn : ('a -> unit) -> 'a -> unit
 
diff --git a/test-suite/success/ProgramWf.v b/test-suite/success/ProgramWf.v
index a6a0da878..18111f07c 100644
--- a/test-suite/success/ProgramWf.v
+++ b/test-suite/success/ProgramWf.v
@@ -1,4 +1,6 @@
 Require Import Arith Program.
+Require Import ZArith Zwf.
+
 Set Implicit Arguments.
 (* Set Printing All. *)
 Print sigT_rect.
@@ -13,11 +15,8 @@ Program Fixpoint merge (n m : nat) {measure (n + m) (lt)} : nat :=
 
 Print merge.
 
-Require Import ZArith.
-
 
 Print Zlt.
-Require Import Zwf.
 Print Zwf.
 
 Open Local Scope Z_scope.
@@ -95,4 +94,3 @@ Qed.
 Program Fixpoint check_n'  (n : nat) (m : nat | m = n) (p : nat) (q : nat | q = p)
   {measure (p - n) p} : nat :=
   _.
-
diff --git a/test-suite/success/autointros.v b/test-suite/success/autointros.v
new file mode 100644
index 000000000..71054e141
--- /dev/null
+++ b/test-suite/success/autointros.v
@@ -0,0 +1,15 @@
+Set Automatic Introduction.
+
+Inductive even : nat -> Prop :=
+| even_0 : even 0
+| even_odd : forall n, odd n -> even (S n)
+with odd : nat -> Prop :=
+| odd_1 : odd 1
+| odd_even : forall n, even n -> odd (S n).
+
+Lemma foo {n : nat} (E : even n) : even (S (S n))
+with bar {n : nat} (O : odd n) : odd (S (S n)).
+Proof. destruct E. constructor. constructor. apply even_odd. apply (bar _ H). 
+  destruct O. repeat constructor. apply odd_even. apply (foo _ H). 
+Defined.
+
diff --git a/toplevel/command.ml b/toplevel/command.ml
index 3b25f2fa6..1086e8419 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -1095,7 +1095,7 @@ let compute_proof_name = function
       in
       next (Pfedit.get_all_proof_names ()) default_thm_id
 
-let save_remaining_recthms (local,kind) body opaq i (id,(t_i,imps)) =
+let save_remaining_recthms (local,kind) body opaq i (id,(t_i,(_,imps))) =
   match body with
   | None ->
       (match local with
@@ -1212,14 +1212,19 @@ let look_for_mutual_statements thms =
 (* 4.2| General support for goals *)
 
 let start_proof_com kind thms hook =
+  let evdref = ref (create_evar_defs Evd.empty) in
+  let env = Global.env () in
   let thms = List.map (fun (sopt,(bl,t)) ->
-    (compute_proof_name sopt,
-     interp_type_evars_impls (Global.env()) (generalize_constr_expr t bl)))
+    let (env, ctx), imps = interp_context_evars evdref env bl in
+    let t', imps' = interp_type_evars_impls ~evdref env t in
+    let len = List.length ctx in
+      (compute_proof_name sopt,
+      (nf_isevar !evdref (it_mkProd_or_LetIn t' ctx), (len, imps @ lift_implicits len imps'))))
     thms in
   let rec_tac,thms = look_for_mutual_statements thms in
   match thms with
   | [] -> anomaly "No proof to start"
-  | (id,(t,imps))::other_thms ->
+  | (id,(t,(len,imps)) as thm)::other_thms ->
       let hook strength ref =
         let other_thms_data =
           if other_thms = [] then [] else
@@ -1230,8 +1235,14 @@ let start_proof_com kind thms hook =
         List.iter (fun (strength,ref,imps) ->
 	  maybe_declare_manual_implicits false ref imps;
 	  hook strength ref) thms_data in
-      start_proof id kind t ?init_tac:rec_tac
-	~compute_guard:(rec_tac<>None) hook
+      let init_tac = 
+	let intro_tac (_, (_, (len, _))) = Refiner.tclDO len Tactics.intro in
+	  if Flags.is_auto_intros () then
+	    match rec_tac with
+ 	    | None -> Some (intro_tac thm)
+	    | Some tac -> Some (Tacticals.tclTHENS tac (List.map intro_tac thms))
+	  else rec_tac
+      in start_proof id kind t ?init_tac hook ~compute_guard:(rec_tac<>None)
 
 let check_anonymity id save_ident =
   if atompart_of_id id <> "Unnamed_thm" then
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 7cde4f637..5ee98db59 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -842,6 +842,14 @@ let _ =
 let _ =
   declare_bool_option
     { optsync  = true;
+      optname  = "automatic introduction of variables";
+      optkey   = ["Automatic";"Introduction"];
+      optread  = Flags.is_auto_intros;
+      optwrite = make_auto_intros }
+
+let _ =
+  declare_bool_option
+    { optsync  = true;
       optname  = "coercion printing";
       optkey   = ["Printing";"Coercions"];
       optread  = (fun () -> !Constrextern.print_coercions);