diff options
| author | Matthieu Sozeau | 2014-11-22 19:34:25 +0100 |
|---|---|---|
| committer | Matthieu Sozeau | 2014-11-23 15:28:41 +0100 |
| commit | ff0a051caf031fb427007714f6325c74b8893702 (patch) | |
| tree | fbb4b2fae772c9a0fe6a8b5d7310eb60dae7c045 /library | |
| parent | c81065e5cdc6d803bd67eccf93dc8fbb640c6892 (diff) | |
Pass around information on the use of template polymorphism for
inductive types (i.e., ones declared with an explicit anonymous Type
at the conclusion of their arity). With this change one can force
inductives to live in higher universes even in the non-fully universe
polymorphic case (e.g. bug #3821).
Diffstat (limited to 'library')
| -rw-r--r-- | library/declare.ml | 1 | ||||
| -rw-r--r-- | library/universes.ml | 11 |
2 files changed, 8 insertions, 4 deletions
diff --git a/library/declare.ml b/library/declare.ml index fb6e1c9b81..56c789c1ed 100644 --- a/library/declare.ml +++ b/library/declare.ml @@ -353,6 +353,7 @@ let discharge_inductive ((sp,kn),(dhyps,mie)) = let dummy_one_inductive_entry mie = { mind_entry_typename = mie.mind_entry_typename; mind_entry_arity = mkProp; + mind_entry_template = false; mind_entry_consnames = mie.mind_entry_consnames; mind_entry_lc = [] } diff --git a/library/universes.ml b/library/universes.ml index 438e6cc532..d69386ddf9 100644 --- a/library/universes.ml +++ b/library/universes.ml @@ -957,10 +957,13 @@ let is_direct_sort_constraint s v = match s with let solve_constraints_system levels level_bounds level_min = let open Univ in let levels = - Array.map (Option.map - (fun u -> match Universe.level u with - | Some u -> u - | _ -> Errors.anomaly (Pp.str"expects Atom"))) + Array.mapi (fun i o -> + match o with + | Some u -> + (match Universe.level u with + | Some u -> Some u + | _ -> level_bounds.(i) <- Universe.sup level_bounds.(i) u; None) + | None -> None) levels in let v = Array.copy level_bounds in let nind = Array.length v in |