- Reforme de la gestion des args recursifs (via arbres reguliers)

- coqtop -byte -opt bouclait!


git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2475 85f007b7-540e-0410-9357-904b9bb8a0f7

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