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/environ.ml | |
| parent | 6a7bcfc6d22ab3bf38847fa3fd05ec194187ff50 (diff) | |
Simplify fresh_foo_instance functions and pretyping of univ instance
Diffstat (limited to 'kernel/environ.ml')
| -rw-r--r-- | kernel/environ.ml | 14 |
1 files changed, 5 insertions, 9 deletions
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 |