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, 10 insertions, 1 deletions

diff --git a/library/libnames.ml b/library/libnames.ml
index 17fd50b7f..2fe8f724c 100644
--- a/library/libnames.ml
+++ b/library/libnames.ml
@@ -23,7 +23,7 @@ type global_reference =
 let subst_global subst ref = match ref with
   | VarRef _ -> ref
   | ConstRef kn ->
-      let kn' = subst_kn subst kn in if kn==kn' then ref else
+      let kn' = subst_con subst kn in if kn==kn' then ref else
           ConstRef kn'
   | IndRef (kn,i) ->
       let kn' = subst_kn subst kn in if kn==kn' then ref else
@@ -190,6 +190,8 @@ type extended_global_reference =
 
 let encode_kn dir id = make_kn (MPfile dir) empty_dirpath (label_of_id id)
 
+let encode_con dir id = make_con (MPfile dir) empty_dirpath (label_of_id id)
+
 let decode_kn kn = 
   let mp,sec_dir,l = repr_kn kn in
     match mp,(repr_dirpath sec_dir) with
@@ -197,6 +199,13 @@ let decode_kn kn =
       | _ , [] -> anomaly "MPfile expected!"
       | _ -> anomaly "Section part should be empty!"
 
+let decode_con kn = 
+  let mp,sec_dir,l = repr_con kn in
+    match mp,(repr_dirpath sec_dir) with
+	MPfile dir,[] -> (dir,id_of_label l)
+      | _ , [] -> anomaly "MPfile expected!"
+      | _ -> anomaly "Section part should be empty!"
+
 (*s qualified names *)
 type qualid = section_path