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, 9 insertions, 8 deletions

diff --git a/library/declare.ml b/library/declare.ml
index ea986e3fb..ecf223ae0 100644
--- a/library/declare.ml
+++ b/library/declare.ml
@@ -142,9 +142,9 @@ let cache_constant ((sp,kn),(cdt,kind)) =
     errorlabstrm "cache_constant" (pr_id id ++ str " already exists"));
   let _,dir,_ = repr_kn kn in
   let kn' = Global.add_constant dir (basename sp) cdt in
-    if kn' <> kn then
+    if kn' <> (constant_of_kn kn) then
       anomaly "Kernel and Library names do not match";
-  Nametab.push (Nametab.Until 1) sp (ConstRef kn);
+  Nametab.push (Nametab.Until 1) sp (ConstRef kn');
   csttab := Spmap.add sp kind !csttab
 
 (* At load-time, the segment starting from the module name to the discharge *)
@@ -154,11 +154,11 @@ let load_constant i ((sp,kn),(_,kind)) =
     let (_,id) = repr_path sp in
     errorlabstrm "cache_constant" (pr_id id ++ str " already exists"));
   csttab := Spmap.add sp kind !csttab;
-  Nametab.push (Nametab.Until i) sp (ConstRef kn)
+  Nametab.push (Nametab.Until i) sp (ConstRef (constant_of_kn kn))
 
 (* Opening means making the name without its module qualification available *)
 let open_constant i ((sp,kn),_) =
-  Nametab.push (Nametab.Exactly i) sp (ConstRef kn)
+  Nametab.push (Nametab.Exactly i) sp (ConstRef (constant_of_kn kn))
 
 (* Hack to reduce the size of .vo: we keep only what load/open needs *)
 let dummy_constant_entry = ConstantEntry (ParameterEntry mkProp)
@@ -190,16 +190,17 @@ let hcons_constant_declaration = function
 
 let declare_constant_common id discharged_hyps (cd,kind) =
   let (sp,kn as oname) = add_leaf id (in_constant (cd,kind)) in
+  let kn = constant_of_kn kn in
   declare_constant_implicits kn;
   Symbols.declare_ref_arguments_scope (ConstRef kn);
   Dischargedhypsmap.set_discharged_hyps sp discharged_hyps;
-  oname
+  kn
 
 let declare_constant_gen internal id (cd,kind) =
   let cd = hcons_constant_declaration cd in
-  let oname = declare_constant_common id [] (ConstantEntry cd,kind) in
-  !xml_declare_constant (internal,oname);
-  oname
+  let kn = declare_constant_common id [] (ConstantEntry cd,kind) in
+  !xml_declare_constant (internal,kn);
+  kn
 
 let declare_internal_constant = declare_constant_gen true
 let declare_constant = declare_constant_gen false