From 0a84134bdd686e3dc0846df6b33d0610cf75c149 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Wed, 9 Jun 2010 10:09:05 +0000
Subject: 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
---
 test-suite/success/RecTutorial.v | 6 ++----
 1 file changed, 2 insertions(+), 4 deletions(-)

(limited to 'test-suite/success/RecTutorial.v')

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
-- 
cgit v1.2.3