diff options
| author | Matthieu Sozeau | 2016-10-21 17:26:36 +0200 |
|---|---|---|
| committer | Matthieu Sozeau | 2016-10-21 17:26:36 +0200 |
| commit | f667e270116aaf46f1c27b5a925d3ffaf0d31365 (patch) | |
| tree | 7ff4fc612585ab7b103b9148e13c35fa21ad3389 /test-suite | |
| parent | 5b0b6c92354c34a4f0d5551f88b16264fb08be5f (diff) | |
| parent | 6b02759513b1ccc7debe87ad9ae6bc6f1341ff6c (diff) | |
Merge branch 'fixminimization' into v8.6
Diffstat (limited to 'test-suite')
| -rw-r--r-- | test-suite/bugs/closed/4527.v | 6 | ||||
| -rw-r--r-- | test-suite/bugs/closed/4544.v | 4 |
2 files changed, 5 insertions, 5 deletions
diff --git a/test-suite/bugs/closed/4527.v b/test-suite/bugs/closed/4527.v index 4ca6fe78cd..08628377f0 100644 --- a/test-suite/bugs/closed/4527.v +++ b/test-suite/bugs/closed/4527.v @@ -249,10 +249,10 @@ Section Reflective_Subuniverse. exact H. Defined. - Definition inO_paths@{i j} (S : Type@{i}) {S_inO : In@{Ou Oa i} O S} (x y : + Definition inO_paths@{i} (S : Type@{i}) {S_inO : In@{Ou Oa i} O S} (x y : S) : In@{Ou Oa i} O (x=y). Proof. - simple refine (inO_to_O_retract@{i j} _ _ _); intro u. + simple refine (inO_to_O_retract@{i} _ _ _); intro u. - assert (p : (fun _ : O (x=y) => x) == (fun _=> y)). { @@ -264,4 +264,4 @@ S) : In@{Ou Oa i} O (x=y). hnf. rewrite O_indpaths_beta; reflexivity. Qed. - Check inO_paths@{Type Type}. + Check inO_paths@{Type}. diff --git a/test-suite/bugs/closed/4544.v b/test-suite/bugs/closed/4544.v index 048f31ce3d..da140c9318 100644 --- a/test-suite/bugs/closed/4544.v +++ b/test-suite/bugs/closed/4544.v @@ -652,7 +652,7 @@ Defined. Definition ReflectiveSubuniverse := Modality. - Definition O_reflector := O_reflector. + Definition O_reflector@{u a i} := O_reflector@{u a i}. Definition In@{u a i} : forall (O : ReflectiveSubuniverse@{u a}), Type2le@{i a} -> Type2le@{i a} @@ -660,7 +660,7 @@ Defined. Definition O_inO@{u a i} : forall (O : ReflectiveSubuniverse@{u a}) (T : Type@{i}), In@{u a i} O (O_reflector@{u a i} O T) := O_inO@{u a i}. - Definition to := to. + Definition to@{u a i} := to@{u a i}. Definition inO_equiv_inO@{u a i j k} : forall (O : ReflectiveSubuniverse@{u a}) (T : Type@{i}) (U : Type@{j}) (T_inO : In@{u a i} O T) (f : T -> U) (feq : IsEquiv f), |