diff options
Diffstat (limited to 'kernel/environ.mli')
| -rw-r--r-- | kernel/environ.mli | 14 |
1 files changed, 6 insertions, 8 deletions
diff --git a/kernel/environ.mli b/kernel/environ.mli index 9a00f053ac..ecaa4d1082 100644 --- a/kernel/environ.mli +++ b/kernel/environ.mli @@ -71,14 +71,20 @@ val add_mind : (* raises [Not_found] if the index points out of the context *) val lookup_rel : int -> env -> rel_declaration +val evaluable_rel_decl : env -> int -> bool + (* Looks up in the context of local vars referred by names ([named_context]) *) (* raises [Not_found] if the identifier is not found *) val lookup_named : variable -> env -> named_declaration +val evaluable_named_decl : env -> variable -> bool + (* Looks up in the context of global constant names *) (* raises [Not_found] if the required path is not found *) val lookup_constant : constant -> env -> constant_body +val evaluable_constant : env -> constant -> bool + (*s [constant_value env c] raises [NotEvaluableConst Opaque] if [c] is opaque and [NotEvaluableConst NoBody] if it has no body and [Not_found] if it does not exist in [env] *) @@ -102,14 +108,6 @@ val vars_of_global : env -> constr -> identifier list val keep_hyps : env -> Idset.t -> section_context -(* A constant is defined when it has a body (theorems do) *) -val defined_constant : env -> constant -> bool -(* A constant is evaluable when delta reduction applies (theorems don't) *) -val evaluable_constant : env -> constant -> bool - -val evaluable_named_decl : env -> variable -> bool -val evaluable_rel_decl : env -> int -> bool - (*s Modules. *) type compiled_env |