diff options
| author |  Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2015-06-23 15:40:16 +0200 |
|---|---|---|
| committer | Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2015-06-26 16:26:30 +0200 |
| commit | d9ac4c22a3a6543959d413120304e356d625c0f9 (patch) | |
| tree | 55379f83d5a3a26a3ebae76d2efb80e2cc09ee9e /test-suite/bugs/closed/3922.v | |
| parent | 3e0aa07cfb1d552e11b37aaf5f0224bfb5b47523 (diff) | |
Fix bug #4254 with the help of J.H. Jourdan
1) We now _assign_ the smallest possible arities to mutual inductive types
and eventually add leq constraints on the user given arities. Remove
useless limitation on instantiating algebraic universe variables with
their least upper bound if they have upper constraints as well.
2) Do not remove non-recursive variables when computing minimal levels of inductives.
3) Avoid modifying user-given arities if not necessary to compute the
minimal level of an inductive.
4) We correctly solve the recursive equations taking into account the
user-declared level.
Diffstat (limited to 'test-suite/bugs/closed/3922.v')
| -rw-r--r-- | test-suite/bugs/closed/3922.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/test-suite/bugs/closed/3922.v b/test-suite/bugs/closed/3922.v index 932084891..0ccc92067 100644 --- a/test-suite/bugs/closed/3922.v +++ b/test-suite/bugs/closed/3922.v @@ -43,7 +43,7 @@ Notation IsHProp := (IsTrunc -1). Monomorphic Axiom dummy_funext_type : Type0. Monomorphic Class Funext := { dummy_funext_value : dummy_funext_type }. -Inductive Unit : Type1 := +Inductive Unit : Set := tt : Unit. Record TruncType (n : trunc_index) := BuildTruncType { |