diff options
Diffstat (limited to 'library/univops.ml')
| -rw-r--r-- | library/univops.ml | 39 |
1 files changed, 0 insertions, 39 deletions
diff --git a/library/univops.ml b/library/univops.ml index 669be2d45..3bafb824d 100644 --- a/library/univops.ml +++ b/library/univops.ml @@ -8,7 +8,6 @@ open Term open Univ -open Declarations let universes_of_constr c = let rec aux s c = @@ -21,44 +20,6 @@ let universes_of_constr c = | _ -> fold_constr aux s c in aux LSet.empty c -let universes_of_inductive mind = - let process auctx = - let u = Univ.AUContext.instance auctx in - let univ_of_one_ind oind = - let arity_univs = - Context.Rel.fold_outside - (fun decl unvs -> - Univ.LSet.union - (Context.Rel.Declaration.fold_constr - (fun cnstr unvs -> - let cnstr = Vars.subst_instance_constr u cnstr in - Univ.LSet.union - (universes_of_constr cnstr) unvs) - decl Univ.LSet.empty) unvs) - oind.mind_arity_ctxt ~init:Univ.LSet.empty - in - Array.fold_left (fun unvs cns -> - let cns = Vars.subst_instance_constr u cns in - Univ.LSet.union (universes_of_constr cns) unvs) arity_univs - oind.mind_nf_lc - in - let univs = - Array.fold_left - (fun unvs pk -> - Univ.LSet.union - (univ_of_one_ind pk) unvs - ) - Univ.LSet.empty mind.mind_packets - in - let mindcnt = Univ.UContext.constraints (Univ.instantiate_univ_context auctx) in - let univs = Univ.LSet.union univs (Univ.universes_of_constraints mindcnt) in - univs - in - match mind.mind_universes with - | Monomorphic_ind _ -> LSet.empty - | Polymorphic_ind auctx -> process auctx - | Cumulative_ind cumi -> process (Univ.ACumulativityInfo.univ_context cumi) - let restrict_universe_context (univs,csts) s = (* Universes that are not necessary to typecheck the term. E.g. univs introduced by tactics and not used in the proof term. *) |