diff options
| author | sacerdot | 2004-11-16 12:37:40 +0000 |
|---|---|---|
| committer | sacerdot | 2004-11-16 12:37:40 +0000 |
| commit | d6c204c70c3b89b5bda4e7779cc4a20b5fa3f63f (patch) | |
| tree | ed4d954a685588ee55f4d8902eba8a1afc864472 /kernel/names.ml | |
| parent | 08cb37edb71af0301a72acc834d50f24b0733db5 (diff) | |
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
Diffstat (limited to 'kernel/names.ml')
| -rw-r--r-- | kernel/names.ml | 16 |
1 files changed, 14 insertions, 2 deletions
diff --git a/kernel/names.ml b/kernel/names.ml index 8211cf845b..db1b1b6df8 100644 --- a/kernel/names.ml +++ b/kernel/names.ml @@ -273,6 +273,9 @@ end module KNmap = Map.Make(KNord) module KNpred = Predicate.Make(KNord) module KNset = Set.Make(KNord) +module Cmap = KNmap +module Cpred = KNpred +module Cset = KNset let default_module_name = id_of_string "If you see this, it's a bug" @@ -288,6 +291,15 @@ type mutual_inductive = kernel_name type inductive = mutual_inductive * int type constructor = inductive * int +let constant_of_kn kn = kn +let make_con mp dir l = (mp,dir,l) +let repr_con con = con +let string_of_con = string_of_kn +let con_label = label +let pr_con = pr_kn +let con_modpath = modpath +let subst_con = subst_kn + let ith_mutual_inductive (kn,_) i = (kn,i) let ith_constructor_of_inductive ind i = (ind,i) let inductive_of_constructor (ind,i) = ind @@ -373,12 +385,12 @@ let hcons_names () = let huniqid = Hashcons.simple_hcons Huniqid.f (hstring,hdir) in let hmod = Hashcons.simple_hcons Hmod.f (hdir,huniqid,hstring) in let hkn = Hashcons.simple_hcons Hkn.f (hmod,hdir,hstring) in - (hkn,hdir,hname,hident,hstring) + (hkn,hkn,hdir,hname,hident,hstring) (*******) -type transparent_state = Idpred.t * KNpred.t +type transparent_state = Idpred.t * Cpred.t type 'a tableKey = | ConstKey of constant |