diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-06-09 10:09:05 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-06-09 10:09:05 +0000 |
| commit | 0a84134bdd686e3dc0846df6b33d0610cf75c149 (patch) | |
| tree | f18c5b29b5361aaf250895bc3d7a3ea636494a0e /test-suite/success/RecTutorial.v | |
| parent | cb586ea65a1ad38626b7481ff8b30007f488705d (diff) | |
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
Diffstat (limited to 'test-suite/success/RecTutorial.v')
| -rw-r--r-- | test-suite/success/RecTutorial.v | 6 |
1 files changed, 2 insertions, 4 deletions
diff --git a/test-suite/success/RecTutorial.v b/test-suite/success/RecTutorial.v index 14d27924e..d4e6a82ef 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 |