diff options
| author | pboutill | 2011-02-10 14:11:01 +0000 |
|---|---|---|
| committer | pboutill | 2011-02-10 14:11:01 +0000 |
| commit | 6df4e0fe6bc6076bc95a1a71d28ae049d04ba517 (patch) | |
| tree | 6e749cf9e23637a28185daac6fb2e12a3d0d6ab4 /theories/Vectors/VectorDef.v | |
| parent | 533c5085e4f9ce392a87841ab67e45c557aa769e (diff) | |
Data structure telling implicits of local variables is a map in the
intern_env
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13823 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/Vectors/VectorDef.v')
| -rw-r--r-- | theories/Vectors/VectorDef.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/theories/Vectors/VectorDef.v b/theories/Vectors/VectorDef.v index e5bb66a20d..150342ee86 100644 --- a/theories/Vectors/VectorDef.v +++ b/theories/Vectors/VectorDef.v @@ -34,8 +34,8 @@ Section SCHEMES. (** An induction scheme for non-empty vectors *) Definition rectS {A} (P:forall {n}, t A (S n) -> Type) - (bas: forall a: A, P 0 (a :: [])) - (rect: forall a {n} (v: t A (S n)), P n v -> P (S n) (a :: v)) := + (bas: forall a: A, P (a :: [])) + (rect: forall a {n} (v: t A (S n)), P v -> P (a :: v)) := fix rectS_fix {n} (v: t A (S n)) : P n v := match v with |nil => @id |