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

diff --git a/toplevel/class.ml b/toplevel/class.ml
index 3d468d3281..c9ed58c795 100644
--- a/toplevel/class.ml
+++ b/toplevel/class.ml
@@ -150,7 +150,7 @@ let uniform_cond nargs lt =
 let id_of_cl  = function
   | CL_FUN -> id_of_string "FUNCLASS"
   | CL_SORT -> id_of_string "SORTCLASS"
-  | CL_CONST kn -> id_of_label (label kn)
+  | CL_CONST kn -> id_of_label (con_label kn)
   | CL_IND ind ->
       let (_,mip) = Global.lookup_inductive ind in
       mip.mind_typename
@@ -271,7 +271,7 @@ let build_id_coercion idf_opt source =
 	const_entry_type = Some typ_f;
         const_entry_opaque = false;
 	const_entry_boxed = Options.boxed_definitions()} in
-  let (_,kn) = declare_constant idf (constr_entry,Decl_kinds.IsDefinition) in
+  let kn = declare_constant idf (constr_entry,Decl_kinds.IsDefinition) in
   ConstRef kn
 
 let check_source = function
@@ -390,13 +390,17 @@ let defined_in_sec kn olddir =
   let _,dir,_ = repr_kn kn in
     dir = olddir
 
+let con_defined_in_sec kn olddir = 
+  let _,dir,_ = repr_con kn in
+    dir = olddir
+
 (* This moves the global path one step below *)
 let process_global olddir = function
   | VarRef _ ->
       anomaly "process_global only processes global surviving the section"
   | ConstRef kn as x ->
-      if defined_in_sec kn olddir then
-        let newkn = Lib.make_kn (id_of_label (label kn)) in
+      if con_defined_in_sec kn olddir then
+        let newkn = Lib.make_con (id_of_label (con_label kn)) in
         ConstRef newkn
       else x
   | IndRef (kn,i) as x -> 
@@ -416,8 +420,8 @@ let process_class olddir ids_to_discard x =
   match cl with 
     | CL_SECVAR _ -> x
     | CL_CONST kn -> 
-       if defined_in_sec kn olddir then
-         let newkn = Lib.make_kn (id_of_label (label kn)) in
+       if con_defined_in_sec kn olddir then
+         let newkn = Lib.make_con (id_of_label (con_label kn)) in
 	 let hyps = (Global.lookup_constant kn).const_hyps in
 	 let n = count_extra_abstractions hyps ids_to_discard in
            (CL_CONST newkn,{cl_strength=stre;cl_param=p+n})
@@ -437,8 +441,8 @@ let process_cl sec_sp cl =
   match cl with
     | CL_SECVAR id -> cl
     | CL_CONST kn ->
-	if defined_in_sec kn sec_sp then
-          let newkn = Lib.make_kn (id_of_label (label kn)) in
+	if con_defined_in_sec kn sec_sp then
+          let newkn = Lib.make_con (id_of_label (con_label kn)) in
           CL_CONST newkn
         else 
 	  cl