diff options
| author | Hugo Herbelin | 2018-10-29 11:27:15 +0100 |
|---|---|---|
| committer | Maxime Dénès | 2018-10-31 16:16:41 +0100 |
| commit | d1091555104e0198eaaa94a1bb69e96d5cc73447 (patch) | |
| tree | dd5f0704a368604e27944c48b1a735c9ab4a8369 /kernel/environ.ml | |
| parent | ae39925d64cc51663ab3f2ad397501b435bd0e5e (diff) | |
Seeing Global purely as a wrapper on top of kernel functions.
Diffstat (limited to 'kernel/environ.ml')
| -rw-r--r-- | kernel/environ.ml | 26 |
1 files changed, 26 insertions, 0 deletions
diff --git a/kernel/environ.ml b/kernel/environ.ml index 3b7e3ae544..e341412294 100644 --- a/kernel/environ.ml +++ b/kernel/environ.ml @@ -440,6 +440,16 @@ let constant_value_and_type env (kn, u) = | Undef _ -> None in b', cb.const_type, Univ.Constraint.empty +let body_of_constant_body env cb = + let otab = opaque_tables env in + match cb.const_body with + | Undef _ -> + None + | Def c -> + Some (Mod_subst.force_constr c, Declareops.constant_polymorphic_context cb) + | OpaqueDef o -> + Some (Opaqueproof.force_proof otab o, Declareops.constant_polymorphic_context cb) + (* These functions should be called under the invariant that [env] already contains the constraints corresponding to the constant application. *) @@ -694,6 +704,22 @@ let is_polymorphic env r = | IndRef ind -> polymorphic_ind ind env | ConstructRef cstr -> polymorphic_ind (inductive_of_constructor cstr) env +let is_template_polymorphic env r = + let open Names.GlobRef in + match r with + | VarRef _id -> false + | ConstRef _c -> false + | IndRef ind -> template_polymorphic_ind ind env + | ConstructRef cstr -> template_polymorphic_ind (inductive_of_constructor cstr) env + +let is_type_in_type env r = + let open Names.GlobRef in + match r with + | VarRef _id -> false + | ConstRef c -> type_in_type_constant c env + | IndRef ind -> type_in_type_ind ind env + | ConstructRef cstr -> type_in_type_ind (inductive_of_constructor cstr) env + (*spiwack: the following functions assemble the pieces of the retroknowledge note that the "consistent" register function is available in the module Safetyping, Environ only synchronizes the proactive and the reactive parts*) |