diff options
| author | Matthieu Sozeau | 2016-10-10 17:28:05 +0200 |
|---|---|---|
| committer | Matthieu Sozeau | 2016-10-20 17:53:14 +0200 |
| commit | ecaea9a428c052ea431ec7c392e81aaf918d5d96 (patch) | |
| tree | 6ef8e9a62ded2734d307e7f917d4c310f893aa6a /test-suite | |
| parent | 3e536acf2ebcd078314dcac2a79d267c95db7bf8 (diff) | |
Fix minimization to be insensitive to redundant arcs.
The new algorithm produces different sets of arcs than in 8.5, hence
existing developments may fail to pass now because they relied on
the (correct but more approximate) result of minimization in 8.5 which
wasn't insensitive.
The algorithm works bottom-up on the (well-founded) graph to
find lower levels that an upper level can be minimized to. We
filter said lower levels according to the lower sets of the other levels
we consider. If they appear in any of them then we don't need their
constraints. Does not seem to have a huge impact on performance in HoTT,
but this should be evaluated further.
Adapt test-suite files accordingly.
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), |