diff options
| author | Gaëtan Gilbert | 2018-10-30 00:10:50 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2018-11-27 13:12:52 +0100 |
| commit | fb4978ce2cf0a2d4fc871d5d739eda8618a5184b (patch) | |
| tree | 85ac88a24bdaf956131869b634a41de23db41694 /test-suite | |
| parent | f6a2d21b6c2a93cb70fde235fc897fb75ea51384 (diff) | |
Fix #8364: making univ algebraic when already equal to another.
When making a universe a variable we iterate through the universes
we're equal to and if we find one we update the substitution
accordingly.
NB: The bug called make_flexible_variable on Top.15 and
~~~
{Top.15 Top.14} |= Top.11 < Top.6
Top.14 < Top.5
Top.11 = Top.15
ALGEBRAIC UNIVERSES:{Top.17 Top.16}
UNDEFINED UNIVERSES:Top.17 := Top.14+1
Top.16 := Top.14+1
WEAK CONSTRAINTS:
~~~
so now we would add [Top.15 := Top.11].
Diffstat (limited to 'test-suite')
| -rw-r--r-- | test-suite/bugs/closed/bug_8364.v | 17 |
1 files changed, 17 insertions, 0 deletions
diff --git a/test-suite/bugs/closed/bug_8364.v b/test-suite/bugs/closed/bug_8364.v new file mode 100644 index 0000000000..10f955b41f --- /dev/null +++ b/test-suite/bugs/closed/bug_8364.v @@ -0,0 +1,17 @@ +Unset Primitive Projections. + +Record Box (A:Type) := box { unbox : A }. +Arguments box {_} _. Arguments unbox {_} _. + +Definition map {A B} (f:A -> B) x := + match x with box x => box (f x) end. + +Definition tuple (l : Box Type) : Type := + match l with + | box x => x + end. + +Fail Inductive stack : Type -> Type := +| Stack T foos : + tuple (map stack foos) -> + stack T. |