From d9ac4c22a3a6543959d413120304e356d625c0f9 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Tue, 23 Jun 2015 15:40:16 +0200 Subject: 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. --- test-suite/bugs/closed/3922.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'test-suite/bugs/closed/3922.v') 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 { -- cgit v1.2.3