Minor cleanup around Term_typing

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

1 files changed, 11 insertions, 16 deletions

diff --git a/kernel/term_typing.mli b/kernel/term_typing.mli
index d001a258e..cc6025dab 100644
--- a/kernel/term_typing.mli
+++ b/kernel/term_typing.mli
@@ -9,29 +9,24 @@
 open Names
 open Term
 open Univ
-open Declarations
-open Inductive
 open Environ
+open Declarations
 open Entries
-open Typeops
 
 val translate_local_def : env -> constr * types option ->
-  constr * types * Univ.constraints
-
-val translate_local_assum : env -> types ->
-  types * Univ.constraints
-
-val infer_declaration : env -> constant_entry ->
-  constant_def * constant_type * constraints * bool * Sign.section_context option
+  constr * types * constraints
 
-val build_constant_declaration : env -> 'a ->
-  constant_def * constant_type * constraints * bool * Sign.section_context option -> 
-    constant_body
+val translate_local_assum : env -> types -> types * constraints
 
-val translate_constant : env -> constant -> constant_entry -> constant_body
+val translate_constant : env -> constant_entry -> constant_body
 
 val translate_mind :
   env -> mutual_inductive -> mutual_inductive_entry -> mutual_inductive_body
 
-val translate_recipe :
-  env -> constant -> Cooking.recipe -> constant_body
+val translate_recipe : env -> Cooking.recipe -> constant_body
+
+
+(** Internal functions, mentioned here for debug purpose only *)
+
+val infer_declaration : env -> constant_entry -> Cooking.result
+val build_constant_declaration : env -> Cooking.result -> constant_body