diff options
Diffstat (limited to 'kernel')
| -rw-r--r-- | kernel/environ.ml | 6 | ||||
| -rw-r--r-- | kernel/environ.mli | 1 |
2 files changed, 7 insertions, 0 deletions
diff --git a/kernel/environ.ml b/kernel/environ.ml index 6f2aeab203..63fbaa6a3b 100644 --- a/kernel/environ.ml +++ b/kernel/environ.ml @@ -571,6 +571,12 @@ let is_primitive env c = | Declarations.Primitive _ -> true | _ -> false +let get_primitive env c = + let cb = lookup_constant c env in + match cb.Declarations.const_body with + | Declarations.Primitive p -> Some p + | _ -> None + let is_int63_type env c = match env.retroknowledge.Retroknowledge.retro_int63 with | None -> false diff --git a/kernel/environ.mli b/kernel/environ.mli index dfd9173d10..414ef2b4d7 100644 --- a/kernel/environ.mli +++ b/kernel/environ.mli @@ -248,6 +248,7 @@ val constant_type_in : env -> Constant.t puniverses -> types val constant_opt_value_in : env -> Constant.t puniverses -> constr option val is_primitive : env -> Constant.t -> bool +val get_primitive : env -> Constant.t -> CPrimitives.t option val is_array_type : env -> Constant.t -> bool val is_int63_type : env -> Constant.t -> bool |