diff options
| -rw-r--r-- | kernel/inductive.ml | 5 | ||||
| -rw-r--r-- | kernel/univ.ml | 4 | ||||
| -rw-r--r-- | kernel/univ.mli | 3 | ||||
| -rw-r--r-- | pretyping/pretyping.ml | 2 | ||||
| -rw-r--r-- | test-suite/bugs/closed/4251.v | 17 |
5 files changed, 29 insertions, 2 deletions
diff --git a/kernel/inductive.ml b/kernel/inductive.ml index 87c139f48..a02d5e205 100644 --- a/kernel/inductive.ml +++ b/kernel/inductive.ml @@ -165,7 +165,10 @@ let rec make_subst env = (* to be greater than the level of the argument; this is probably *) (* a useless extra constraint *) let s = sort_as_univ (snd (dest_arity env (Lazy.force a))) in - make (cons_subst u s subst) (sign, exp, args) + if Univ.Universe.is_levels s then + make (cons_subst u s subst) (sign, exp, args) + else (* Cannot handle substitution by i+n universes. *) + make subst (sign, exp, args) | (na,None,t)::sign, Some u::exp, [] -> (* No more argument here: we add the remaining universes to the *) (* substitution (when [u] is distinct from all other universes in the *) diff --git a/kernel/univ.ml b/kernel/univ.ml index 782778d09..73d323426 100644 --- a/kernel/univ.ml +++ b/kernel/univ.ml @@ -553,6 +553,10 @@ struct | Cons (l, _, Nil) -> Expr.is_level l | _ -> false + let rec is_levels l = match l with + | Cons (l, _, r) -> Expr.is_level l && is_levels r + | Nil -> true + let level l = match l with | Cons (l, _, Nil) -> Expr.level l | _ -> None diff --git a/kernel/univ.mli b/kernel/univ.mli index ad33d597e..4cc8a2528 100644 --- a/kernel/univ.mli +++ b/kernel/univ.mli @@ -91,6 +91,9 @@ sig val is_level : t -> bool (** Test if the universe is a level or an algebraic universe. *) + val is_levels : t -> bool + (** Test if the universe is a lub of levels or contains +n's. *) + val level : t -> Level.t option (** Try to get a level out of a universe, returns [None] if it is an algebraic universe. *) diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index edb76e52f..f18657da8 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -645,7 +645,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) env evdref (lvar : ltac_ match evar_kind_of_term !evdref resj.uj_val with | App (f,args) -> let f = whd_evar !evdref f in - if isInd f && is_template_polymorphic env f then + if is_template_polymorphic env f then (* Special case for inductive type applications that must be refreshed right away. *) let sigma = !evdref in diff --git a/test-suite/bugs/closed/4251.v b/test-suite/bugs/closed/4251.v new file mode 100644 index 000000000..66343d667 --- /dev/null +++ b/test-suite/bugs/closed/4251.v @@ -0,0 +1,17 @@ + +Inductive array : Type -> Type := +| carray : forall A, array A. + +Inductive Mtac : Type -> Prop := +| bind : forall {A B}, Mtac A -> (A -> Mtac B) -> Mtac B +| array_make : forall {A}, A -> Mtac (array A). + +Definition Ref := array. + +Definition ref : forall {A}, A -> Mtac (Ref A) := + fun A x=> array_make x. +Check array Type. +Check fun A : Type => Ref A. + +Definition abs_val (a : Type) := + bind (ref a) (fun r : array Type => array_make tt).
\ No newline at end of file |