diff options
| author | Gaëtan Gilbert | 2018-10-10 13:15:06 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2018-10-16 15:51:49 +0200 |
| commit | 72de7e057505c45cdbf75234a9ea90465d0e19ec (patch) | |
| tree | 42c0a83da6b9225f177e873d7040e10e2284e35d /kernel | |
| parent | 6a7bcfc6d22ab3bf38847fa3fd05ec194187ff50 (diff) | |
Simplify fresh_foo_instance functions and pretyping of univ instance
Diffstat (limited to 'kernel')
| -rw-r--r-- | kernel/constr.ml | 6 | ||||
| -rw-r--r-- | kernel/constr.mli | 3 | ||||
| -rw-r--r-- | kernel/environ.ml | 14 |
3 files changed, 14 insertions, 9 deletions
diff --git a/kernel/constr.ml b/kernel/constr.ml index c97969c0e0..7ffde3107b 100644 --- a/kernel/constr.ml +++ b/kernel/constr.ml @@ -227,6 +227,12 @@ let mkMeta n = Meta n (* Constructs a Variable named id *) let mkVar id = Var id +let mkRef (gr,u) = let open GlobRef in match gr with + | ConstRef c -> mkConstU (c,u) + | IndRef ind -> mkIndU (ind,u) + | ConstructRef c -> mkConstructU (c,u) + | VarRef x -> mkVar x + (************************************************************************) (* kind_of_term = constructions as seen by the user *) (************************************************************************) diff --git a/kernel/constr.mli b/kernel/constr.mli index 3c9cc96a0d..12819ac39d 100644 --- a/kernel/constr.mli +++ b/kernel/constr.mli @@ -128,6 +128,9 @@ val mkConstruct : constructor -> constr val mkConstructU : pconstructor -> constr val mkConstructUi : pinductive * int -> constr +(** Make a constant, inductive, constructor or variable. *) +val mkRef : GlobRef.t Univ.puniverses -> constr + (** Constructs a destructor of inductive type. [mkCase ci p c ac] stand for match [c] as [x] in [I args] return [p] with [ac] diff --git a/kernel/environ.ml b/kernel/environ.ml index 1feb47d387..757c8773b7 100644 --- a/kernel/environ.ml +++ b/kernel/environ.ml @@ -419,12 +419,6 @@ let constant_type env (kn,u) = let csts = constraints_of cb u in (subst_instance_constr u cb.const_type, csts) -let constant_context env kn = - let cb = lookup_constant kn env in - match cb.const_universes with - | Monomorphic_const _ -> Univ.AUContext.empty - | Polymorphic_const ctx -> ctx - type const_evaluation_result = NoBody | Opaque exception NotEvaluableConst of const_evaluation_result @@ -551,13 +545,15 @@ let lookup_constructor_variables (ind,_) env = lookup_inductive_variables ind env (* Universes *) +let constant_context env c = + let cb = lookup_constant c env in + Declareops.constant_polymorphic_context cb + let universes_of_global env r = let open GlobRef in match r with | VarRef _ -> Univ.AUContext.empty - | ConstRef c -> - let cb = lookup_constant c env in - Declareops.constant_polymorphic_context cb + | ConstRef c -> constant_context env c | IndRef (mind,_) | ConstructRef ((mind,_),_) -> let mib = lookup_mind mind env in Declareops.inductive_polymorphic_context mib |