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

2 files changed, 17 insertions, 4 deletions

diff --git a/test-suite/success/ProgramWf.v b/test-suite/success/ProgramWf.v
index a6a0da878c..18111f07c5 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 0000000000..71054e1415
--- /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.
+