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

3 files changed, 2 insertions, 6 deletions

diff --git a/test-suite/success/AdvancedCanonicalStructure.v b/test-suite/success/AdvancedCanonicalStructure.v
index c1405cf91f..b533db6eac 100644
--- a/test-suite/success/AdvancedCanonicalStructure.v
+++ b/test-suite/success/AdvancedCanonicalStructure.v
@@ -21,7 +21,6 @@ Parameter eq_img : forall (i1:img) (i2:img),
   eqB (ib i1) (ib i2) -> eqA (ia i1) (ia i2).
 
 Lemma phi_img (a:A) : img.
-  intro a.
   exists  a (phi a).
   refine ( refl_equal _).
 Defined.
diff --git a/test-suite/success/RecTutorial.v b/test-suite/success/RecTutorial.v
index 14d27924ef..d4e6a82ef0 100644
--- a/test-suite/success/RecTutorial.v
+++ b/test-suite/success/RecTutorial.v
@@ -322,7 +322,7 @@ match v in (vector _ n0) return (vector A (pred n0)) with
 end.
 
 Definition Vtail' (A:Set)(n:nat)(v:vector A n) : vector A (pred n).
- intros A n v; case v.
+ case v.
  simpl.
  exact (Vnil A).
  simpl.
@@ -920,9 +920,7 @@ Print minus_decrease.
 
 
 
-Definition div_aux (x y:nat)(H: Acc lt x):nat.
- fix 3.
- intros.
+Fixpoint div_aux (x y:nat)(H: Acc lt x):nat.
   refine (if eq_nat_dec x 0
          then 0
          else if eq_nat_dec y 0
diff --git a/test-suite/success/coercions.v b/test-suite/success/coercions.v
index 3d1c91bbe6..908b5f77d3 100644
--- a/test-suite/success/coercions.v
+++ b/test-suite/success/coercions.v
@@ -71,7 +71,6 @@ Record Morphism (X Y:Setoid) : Type :=
 {evalMorphism :> X -> Y}.
 
 Definition extSetoid (X Y:Setoid) : Setoid.
-intros X Y.
 constructor.
 exact (Morphism X Y).
 Defined.