diff options
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 |