diff options
| author |  Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2015-01-18 00:07:32 +0530 |
|---|---|---|
| committer | Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2015-01-18 00:07:32 +0530 |
| commit | 5e5d51762df0e34769225e8c59c77b97b1212c29 (patch) | |
| tree | 61aa0a74d77089ed4a7db12ff6fc46059ab2fb61 | |
| parent | 9d8347abc07dec1edd804b2fa39db40088b5cf3d (diff) | |
There was one more universe needed due to the use of now non-universe-polymorphic
ID, fixing the script results in 3 universes for the stdlib again.
| -rw-r--r-- | test-suite/Makefile | 2 | ||||
| -rw-r--r-- | theories/Vectors/VectorSpec.v | 6 |
2 files changed, 4 insertions, 4 deletions
diff --git a/test-suite/Makefile b/test-suite/Makefile index 055485d0b..4a3a287c0 100644 --- a/test-suite/Makefile +++ b/test-suite/Makefile @@ -387,7 +387,7 @@ misc/deps-order.log: } > "$@" # Sort universes for the whole standard library -EXPECTED_UNIVERSES := 4 +EXPECTED_UNIVERSES := 3 universes: misc/universes.log misc/universes.log: misc/universes/all_stdlib.v @echo "TEST misc/universes" diff --git a/theories/Vectors/VectorSpec.v b/theories/Vectors/VectorSpec.v index 3e8c1175f..7f4228dd6 100644 --- a/theories/Vectors/VectorSpec.v +++ b/theories/Vectors/VectorSpec.v @@ -62,12 +62,12 @@ Proof. refine (@Fin.rectS _ _ _); lazy beta; [ intros n v | intros n p H v ]. revert n v; refine (@caseS _ _ _); simpl; intros. now destruct t. revert p H. - refine (match v as v' in t _ m return match m as m' return t A m' -> Type with + refine (match v as v' in t _ m return match m as m' return t A m' -> Prop with |S (S n) => fun v => forall p : Fin.t (S n), (forall v0 : t A (S n), (shiftrepeat v0) [@ Fin.L_R 1 p ] = v0 [@p]) -> (shiftrepeat v) [@Fin.L_R 1 (Fin.FS p)] = v [@Fin.FS p] - |_ => fun _ => @ID end v' with - |[] => @id |h :: t => _ end). destruct n0. exact @id. now simpl. + |_ => fun _ => True end v' with + |[] => I |h :: t => _ end). destruct n0. exact I. now simpl. Qed. Lemma shiftrepeat_last A: forall n (v: t A (S n)), last (shiftrepeat v) = last v. |