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, 16 insertions, 2 deletions

diff --git a/kernel/names.mli b/kernel/names.mli
index a08d1be238..8cda7d958d 100644
--- a/kernel/names.mli
+++ b/kernel/names.mli
@@ -158,13 +158,26 @@ module KNmap  : Map.S with type key = kernel_name
 (*s Specific paths for declarations *)
 
 type variable = identifier
-type constant = kernel_name
+type constant
 type mutual_inductive = kernel_name
 (* Beware: first inductive has index 0 *)
 type inductive = mutual_inductive * int
 (* Beware: first constructor has index 1 *)
 type constructor = inductive * int
 
+module Cmap  : Map.S with type key = constant
+module Cpred  : Predicate.S with type elt = constant
+module Cset  : Set.S with type elt = constant
+
+val constant_of_kn : kernel_name -> constant
+val make_con : module_path -> dir_path -> label -> constant
+val repr_con : constant -> module_path * dir_path * label
+val string_of_con : constant -> string
+val con_label : constant -> label
+val con_modpath : constant -> module_path
+val pr_con : constant -> Pp.std_ppcmds
+val subst_con : substitution -> constant -> constant
+
 val ith_mutual_inductive : inductive -> int -> inductive
 val ith_constructor_of_inductive : inductive -> int -> constructor
 val inductive_of_constructor : constructor -> inductive
@@ -177,6 +190,7 @@ type evaluable_global_reference =
 
 (* Hash-consing *)
 val hcons_names : unit ->
+  (constant -> constant) *
   (kernel_name -> kernel_name) * (dir_path -> dir_path) *
   (name -> name) * (identifier -> identifier) * (string -> string)
 
@@ -188,7 +202,7 @@ type 'a tableKey =
   | VarKey of identifier
   | RelKey of 'a 
 
-type transparent_state = Idpred.t * KNpred.t
+type transparent_state = Idpred.t * Cpred.t
 
 type inv_rel_key = int (* index in the [rel_context] part of environment
 			  starting by the end, {\em inverse}