diff options
| author |  Amin Timany <amintimany@gmail.com> | 2017-06-01 16:18:19 +0200 |
|---|---|---|
| committer |  Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-06-16 04:51:19 +0200 |
| commit | ff918e4bb0ae23566e038f4b55d84dd2c343f95e (patch) | |
| tree | ebab76cc4dedaf307f96088a3756d8292a341433 /checker/univ.ml | |
| parent | 3380f47d2bb38d549fcdac8fb073f9aa1f259a23 (diff) | |
Clean up universes of constants and inductives
Diffstat (limited to 'checker/univ.ml')
| -rw-r--r-- | checker/univ.ml | 20 |
1 files changed, 15 insertions, 5 deletions
diff --git a/checker/univ.ml b/checker/univ.ml index 92b6a9e86..0ee4686c1 100644 --- a/checker/univ.ml +++ b/checker/univ.ml @@ -1184,7 +1184,11 @@ end type universe_context = UContext.t -module UInfoInd = +module AUContext = UContext + +type abstract_universe_context = AUContext.t + +module CumulativityInfo = struct type t = universe_context * universe_context @@ -1223,7 +1227,10 @@ struct end -type universe_info_ind = UInfoInd.t +type cumulativity_info = CumulativityInfo.t + +module ACumulativityInfo = CumulativityInfo +type abstract_cumulativity_info = ACumulativityInfo.t module ContextSet = struct @@ -1281,7 +1288,10 @@ let subst_instance_constraint s (u,d,v as c) = let subst_instance_constraints s csts = Constraint.fold (fun c csts -> Constraint.add (subst_instance_constraint s c) csts) - csts Constraint.empty + csts Constraint.empty + +let subst_instance_context inst (inner_inst, inner_constr) = + (inner_inst, subst_instance_constraints inst inner_constr) let make_abstract_instance (ctx, _) = Array.mapi (fun i l -> Level.var i) ctx @@ -1290,8 +1300,8 @@ let make_abstract_instance (ctx, _) = let instantiate_univ_context (ctx, csts) = (ctx, subst_instance_constraints ctx csts) -let instantiate_univ_constraints u (_, csts) = - subst_instance_constraints u csts +let instantiate_cumulativity_info (ctx, ctx') = + (instantiate_univ_context ctx, instantiate_univ_context ctx') (** With level to universe substitutions. *) type universe_subst_fn = universe_level -> universe |