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/modops.ml b/kernel/modops.ml
index 5a0694cbef..aca663e7c9 100644
--- a/kernel/modops.ml
+++ b/kernel/modops.ml
@@ -163,8 +163,9 @@ let subst_signature_msid msid mp =
 let rec add_signature mp sign env = 
   let add_one env (l,elem) =
     let kn = make_kn mp empty_dirpath l in
+    let con = make_con mp empty_dirpath l in
       match elem with
-	| SPBconst cb -> Environ.add_constant kn cb env
+	| SPBconst cb -> Environ.add_constant con cb env
 	| SPBmind mib -> Environ.add_mind kn mib env
 	| SPBmodule mb -> 
 	    add_module (MPdot (mp,l)) (module_body_of_spec mb) env 
@@ -189,7 +190,7 @@ let strengthen_const env mp l cb =
   | false, Some _ -> cb
   | true, Some _ 
   | _, None -> 
-      let const = mkConst (make_kn mp empty_dirpath l) in 
+      let const = mkConst (make_con mp empty_dirpath l) in 
       let const_subs = Some (Declarations.from_val const) in
 	{cb with 
       	   const_body = const_subs;