diff options
author | pboutill <pboutill@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-07-20 14:22:44 +0000 |
---|---|---|
committer | pboutill <pboutill@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-07-20 14:22:44 +0000 |
commit | 88af5db4957e7e866ea507825ff0f08bd09c38ad (patch) | |
tree | e81971a4eb04ff5e0be67d8d5b9e93ae93a1d0ff /theories/Vectors/VectorSpec.v | |
parent | f03aaca003d9903bb90493a472a5f3138572a30e (diff) |
Vector equalities first stuff
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15632 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/Vectors/VectorSpec.v')
-rw-r--r-- | theories/Vectors/VectorSpec.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/theories/Vectors/VectorSpec.v b/theories/Vectors/VectorSpec.v index 2f4086e5c..2d0a75f32 100644 --- a/theories/Vectors/VectorSpec.v +++ b/theories/Vectors/VectorSpec.v @@ -16,7 +16,7 @@ Require Fin. Require Import VectorDef. Import VectorNotations. -Definition cons_inj A a1 a2 n (v1 v2 : t A n) +Definition cons_inj {A} {a1 a2} {n} {v1 v2 : t A n} (eq : a1 :: v1 = a2 :: v2) : a1 = a2 /\ v1 = v2 := match eq in _ = x return caseS _ (fun a2' _ v2' => fun v1' => a1 = a2' /\ v1' = v2') x v1 with | eq_refl => conj eq_refl eq_refl |