Automatic introduction of names given before ":" in Lemma's and

Definition's is not so painless. It seems to however generally provide
"nicer" scripts so let us keep it and update the contribs and
test-suite accordingly.
Also enforced that the actual introduced names to be exactly as given
in the statements.

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

4 files changed, 7 insertions, 7 deletions

diff --git a/test-suite/bugs/closed/shouldsucceed/1643.v b/test-suite/bugs/closed/shouldsucceed/1643.v
index 4114987d36..879a65b183 100644
--- a/test-suite/bugs/closed/shouldsucceed/1643.v
+++ b/test-suite/bugs/closed/shouldsucceed/1643.v
@@ -10,7 +10,6 @@ Definition decomp_func (s:Str) :=
 
 Theorem decomp s: s = decomp_func s.
 Proof.
-  intros s.
   case s; simpl; reflexivity.
 Qed.
 
diff --git a/test-suite/bugs/closed/shouldsucceed/1891.v b/test-suite/bugs/closed/shouldsucceed/1891.v
index 11124cddd7..2d90a2f1dc 100644
--- a/test-suite/bugs/closed/shouldsucceed/1891.v
+++ b/test-suite/bugs/closed/shouldsucceed/1891.v
@@ -7,7 +7,7 @@
 
   Lemma L (x: T unit): (unit -> T unit) -> unit.
   Proof.
-    refine (fun x => match x return _ with mkT n => fun g => f (g _) end).
+    refine (match x return _ with mkT n => fun g => f (g _) end).
     trivial.
   Qed.
 
diff --git a/test-suite/bugs/closed/shouldsucceed/1918.v b/test-suite/bugs/closed/shouldsucceed/1918.v
index 474ec935b2..9d92fe12b8 100644
--- a/test-suite/bugs/closed/shouldsucceed/1918.v
+++ b/test-suite/bugs/closed/shouldsucceed/1918.v
@@ -66,14 +66,14 @@ Definition pEFct (F:k2) : Type :=
 Definition moncomp (X Y:k1)(mX:mon X)(mY:mon Y): mon (fun A => X(Y A)).
 Proof.
   red.
-  intros X Y mX mY A B f x.
+  intros A B f x.
   exact (mX (Y A)(Y B) (mY A B f) x).
 Defined.
 
 (** closure under composition *)
 Lemma compEFct (X Y:k1): EFct X -> EFct Y -> EFct (fun A => X(Y A)).
 Proof.
-  intros X Y ef1 ef2.
+  intros ef1 ef2.
   apply (mkEFct(m:=moncomp (m ef1) (m ef2))); red; intros; unfold moncomp.
 (* prove ext *)
   apply (e ef1).
@@ -103,7 +103,7 @@ Defined.
 (** closure under sums *)
 Lemma sumEFct (X Y:k1): EFct X -> EFct Y -> EFct (fun A => X A + Y A)%type.
 Proof.
-  intros X Y ef1 ef2.
+  intros ef1 ef2.
   set (m12:=fun (A B:Set)(f:A->B) x => match x with
     | inl y => inl _ (m ef1 f y)
     | inr y => inr _ (m ef2 f y)
@@ -144,7 +144,7 @@ Defined.
 (** closure under products *)
 Lemma prodEFct (X Y:k1): EFct X -> EFct Y -> EFct (fun A => X A * Y A)%type.
 Proof.
-  intros X Y ef1 ef2.
+  intros ef1 ef2.
   set (m12:=fun (A B:Set)(f:A->B) x => match x with
     (x1,x2) => (m ef1 f x1, m ef2 f x2) end).
   apply (mkEFct(m:=m12)); red; intros.
@@ -220,7 +220,6 @@ Defined.
 (** constants in k1 *)
 Lemma constEFct (C:Set): EFct (fun _ => C).
 Proof.
-  intro.
   set (mC:=fun A B (f:A->B)(x:C) => x).
   apply (mkEFct(m:=mC)); red; intros; unfold mC; reflexivity.
 Defined.
diff --git a/test-suite/bugs/closed/shouldsucceed/2001.v b/test-suite/bugs/closed/shouldsucceed/2001.v
index c50ad036d7..d0b3bf1732 100644
--- a/test-suite/bugs/closed/shouldsucceed/2001.v
+++ b/test-suite/bugs/closed/shouldsucceed/2001.v
@@ -1,6 +1,8 @@
 (* Automatic computing of guard in "Theorem with"; check that guard is not
    computed when the user explicitly indicated it *)
 
+Unset Automatic Introduction.
+
 Inductive T : Set :=
 | v : T.