diff options
| author |  Matthieu Sozeau <mattam@mattam.org> | 2014-06-23 12:25:32 +0200 |
|---|---|---|
| committer | Matthieu Sozeau <mattam@mattam.org> | 2014-06-23 13:10:02 +0200 |
| commit | 9753da73ed9f1e12d16b7d9b66d0c68b1d015918 (patch) | |
| tree | 12f1ce4fef52eddafc9fa9e6890532e306cf65c8 /test-suite/bugs/closed/HoTT_coq_044.v | |
| parent | 44b149ec1d220d38754545f18a39ef76a3be44b5 (diff) | |
The test-suite file couldn't typecheck as it rightly introduces a universe inconsistency.
One needs to use a universe level lower than eq's parameter for this to be consistent.
Diffstat (limited to 'test-suite/bugs/closed/HoTT_coq_044.v')
| -rw-r--r-- | test-suite/bugs/closed/HoTT_coq_044.v | 7 |
1 files changed, 5 insertions, 2 deletions
diff --git a/test-suite/bugs/closed/HoTT_coq_044.v b/test-suite/bugs/closed/HoTT_coq_044.v index 1a59de092..c824f53ba 100644 --- a/test-suite/bugs/closed/HoTT_coq_044.v +++ b/test-suite/bugs/closed/HoTT_coq_044.v @@ -1,5 +1,7 @@ Require Import Classes.RelationClasses List Setoid. +Definition eqT (T : Type) := @eq T. + Set Universe Polymorphism. Definition RowType := list Type. @@ -17,10 +19,11 @@ Inductive RowTypeDecidable (P : forall T, relation T) `(H : forall T, Equivalenc -> RowTypeDecidable P H Ts -> RowTypeDecidable P H (T :: Ts). + Set Printing Universes. -Fixpoint Row_eq Ts -: RowTypeDecidable (@eq) _ Ts -> forall r1 r2 : Row Ts, {@eq (Row Ts) r1 r2} + {r1 <> r2}. +Fixpoint Row_eq (Ts : RowType) +: RowTypeDecidable (@eqT) _ Ts -> forall r1 r2 : Row Ts, {@eq (Row Ts) r1 r2} + {r1 <> r2}. (* Toplevel input, characters 81-87: Error: In environment |