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 | |
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')
-rw-r--r-- | test-suite/bugs/closed/HoTT_coq_036.v | 6 | ||||
-rw-r--r-- | test-suite/bugs/closed/HoTT_coq_054.v | 4 |
2 files changed, 5 insertions, 5 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 *. diff --git a/test-suite/bugs/closed/HoTT_coq_054.v b/test-suite/bugs/closed/HoTT_coq_054.v index f79fe1c1e..b47bb3a20 100644 --- a/test-suite/bugs/closed/HoTT_coq_054.v +++ b/test-suite/bugs/closed/HoTT_coq_054.v @@ -47,10 +47,10 @@ Theorem ex2_8 {A B A' B' : Type} (g : A -> A') (h : B -> B') (x y : A + B) | inl y' => ap g | inr y' => idmap end - | inr x' => match y as y return match y with + | inr x' => match y as y return match y return Type with inr y' => x' = y' | _ => Empty - end -> match f y with + end -> match f y return Type with | inr y' => h x' = y' | _ => Empty end with | inl y' => idmap |