diff options
| author |  Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2015-10-01 15:36:57 +0200 |
|---|---|---|
| committer |  Matthieu Sozeau <mattam@mattam.org> | 2015-10-02 15:54:13 +0200 |
| commit | b3d97c2147418f44fc704807d3812b04921591af (patch) | |
| tree | 695491ad5693218e18e023ac36671c653cf15c71 /kernel | |
| parent | c1630c9dcdf91dc965b3c375d68e3338fb737531 (diff) | |
Univs: fix bug #4251, handling of template polymorphic constants.
Diffstat (limited to 'kernel')
| -rw-r--r-- | kernel/inductive.ml | 5 | ||||
| -rw-r--r-- | kernel/univ.ml | 4 | ||||
| -rw-r--r-- | kernel/univ.mli | 3 |
3 files changed, 11 insertions, 1 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. *) |