diff options
| author |  Matthieu Sozeau <mattam@mattam.org> | 2014-06-23 13:01:31 +0200 |
|---|---|---|
| committer | Matthieu Sozeau <mattam@mattam.org> | 2014-06-23 13:10:02 +0200 |
| commit | db37c9f3f32ae7a2abcd5e1a3f6239eddb5e1768 (patch) | |
| tree | 6eaead7c3cd3b61ec54295a9037a4ef568b5dedb /test-suite/bugs/closed/HoTT_coq_036.v | |
| parent | 0b1507b16da38e883d63802db7c013e2c09665fd (diff) | |
Fix semantics of change p with c to typecheck c at each specific occurrence of p,
avoiding unwanted universe constraints in presence of universe polymorphic constants.
Fixing HoTT bugs # 36, 54 and 113.
Diffstat (limited to 'test-suite/bugs/closed/HoTT_coq_036.v')
| -rw-r--r-- | test-suite/bugs/closed/HoTT_coq_036.v | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/test-suite/bugs/closed/HoTT_coq_036.v b/test-suite/bugs/closed/HoTT_coq_036.v index f10856bc7..4c3e078a5 100644 --- a/test-suite/bugs/closed/HoTT_coq_036.v +++ b/test-suite/bugs/closed/HoTT_coq_036.v @@ -29,8 +29,8 @@ Module Version1. assert (Hf : focus ((S tt) = (S tt))) by constructor. let C1 := constr:(CObject) in let C2 := constr:(fun C => @Object (CObject C) C) in - unify C1 C2. - progress change CObject with (fun C => @Object (CObject C) C) in *. + unify C1 C2; idtac C1 C2. Show Universes. + progress change @CObject with (fun C => @Object (CObject C) C) in *. simpl in *. match type of Hf with | focus ?V => exact V @@ -112,7 +112,7 @@ Module OtherBug. Parameter ObjectOf' : forall (objC : Type) (C : SpecializedCategory objC) (objD : Type) (D : SpecializedCategory objD), Prop. - Definition CommaCategory_Object (A : Category) : Type. + Definition CommaCategory_Object (A : Category@{i}) : Type. assert (Hf : focus (@ObjectOf' _ (@Build_Category unit TerminalCategory) _ A)) by constructor. progress change CObject with (fun C => @Object (CObject C) C) in *; simpl in *. |