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.ml b/kernel/constant.ml
index 0b52af695..766fbb735 100644
--- a/kernel/constant.ml
+++ b/kernel/constant.ml
@@ -16,17 +16,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
-
 let is_defined cb = 
   match cb.const_body with Some _ -> true | _ -> false