diff options
| author |  Matthieu Sozeau <mattam@mattam.org> | 2016-10-10 17:28:05 +0200 |
|---|---|---|
| committer | Matthieu Sozeau <mattam@mattam.org> | 2016-10-20 17:53:14 +0200 |
| commit | ecaea9a428c052ea431ec7c392e81aaf918d5d96 (patch) | |
| tree | 6ef8e9a62ded2734d307e7f917d4c310f893aa6a /test-suite/bugs/closed/4544.v | |
| 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/bugs/closed/4544.v')
| -rw-r--r-- | test-suite/bugs/closed/4544.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/test-suite/bugs/closed/4544.v b/test-suite/bugs/closed/4544.v index 048f31ce3..da140c931 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), |