IMPORTANT COMMIT: constant is now an ADT (it used to be equal to kernel_name).

MOVITATION: in a forthcoming commit the application of a substitution to a
constant will return a constr and not a constant. The application of a
substitution to a kernel_name will return a kernel_name. Thus "constant"
should be use as a kernel name for references that can be delta-expanded.

KNOWN PROBLEMS: the only problem faced is in pretyping/recordops.ml (the code
that implements "Canonical Structure"s). The ADT is violated once in this
ocaml module. My feeling is that the implementation of "Canonical Structure"s
should be rewritten to avoid this situation.


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

1 files changed, 3 insertions, 2 deletions

diff --git a/kernel/mod_typing.ml b/kernel/mod_typing.ml
index a3639ef988..9f5a5e9a85 100644
--- a/kernel/mod_typing.ml
+++ b/kernel/mod_typing.ml
@@ -143,13 +143,14 @@ and translate_entry_list env msid is_definition sig_e =
   let mp = MPself msid in
   let do_entry env (l,e) = 
     let kn = make_kn mp empty_dirpath l in
+    let con = make_con mp empty_dirpath l in
     match e with
       | SPEconst ce ->
-	  let cb = translate_constant env kn ce in
+	  let cb = translate_constant env con ce in
 	    begin match cb.const_hyps with
 	      |	(_::_) -> error_local_context (Some l)
 	      | [] ->
-		  add_constant kn cb env, (l, SEBconst cb), (l, SPBconst cb)
+		  add_constant con cb env, (l, SEBconst cb), (l, SPBconst cb)
 	    end
       | SPEmind mie -> 
 	  let mib = translate_mind env mie in