environnement sur

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

1 files changed, 5 insertions, 3 deletions

diff --git a/kernel/constant.mli b/kernel/constant.mli
index 60607cef2..d33dc5a85 100644
--- a/kernel/constant.mli
+++ b/kernel/constant.mli
@@ -11,17 +11,19 @@ type recipe =
   | Cooked of constr
   | Recipe of discharge_recipe
 
+type constant_entry = {
+  const_entry_body : constr;
+  const_entry_type : constr }
+
 type constant_body = {
   const_kind : path_kind;
   const_body : recipe ref option;
   const_type : typed_type;
-  const_hyps : context;
+  const_hyps : typed_type signature;
   mutable const_opaque : bool;
   mutable const_eval : ((int * constr) list * int * bool) option option;
 }
 
-type constant_entry = section_path * constant_body
-
 val is_defined : constant_body -> bool
 
 val is_opaque : constant_body -> bool