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/environ.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/environ.ml')
| -rw-r--r-- | kernel/environ.ml | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/kernel/environ.ml b/kernel/environ.ml index d9569bca64..a6d7ff65b9 100644 --- a/kernel/environ.ml +++ b/kernel/environ.ml @@ -29,7 +29,7 @@ type constant_key = constant_body * key type engagement = ImpredicativeSet type globals = { - env_constants : constant_key KNmap.t; + env_constants : constant_key Cmap.t; env_inductives : mutual_inductive_body KNmap.t; env_modules : module_body MPmap.t; env_modtypes : module_type_body KNmap.t } @@ -57,7 +57,7 @@ and env = { let empty_env = { env_globals = { - env_constants = KNmap.empty; + env_constants = Cmap.empty; env_inductives = KNmap.empty; env_modules = MPmap.empty; env_modtypes = KNmap.empty }; @@ -218,13 +218,13 @@ let set_pos_constant (cb,r) bpos = else raise AllReadyEvaluated let lookup_constant_key kn env = - KNmap.find kn env.env_globals.env_constants + Cmap.find kn env.env_globals.env_constants let lookup_constant kn env = constant_key_body (lookup_constant_key kn env) let add_constant kn cs env = let new_constants = - KNmap.add kn (cs,ref notevaluated) env.env_globals.env_constants in + Cmap.add kn (cs,ref notevaluated) env.env_globals.env_constants in let new_globals = { env.env_globals with env_constants = new_constants } in |