diff options
| author | Pierre-Marie Pédrot | 2014-03-07 20:50:30 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2014-03-07 21:00:02 +0100 |
| commit | dd2a0175e3e35e5488c6f3b8a68c68845cbfcfd3 (patch) | |
| tree | 2b61640b942b39650dec17ca077f28b5363aa843 /kernel/environ.ml | |
| parent | 89e59b9a578fa761ebc12e3a8e01c3b838301266 (diff) | |
Using Hashmaps by default in constant and inductive maps. This changes fold and
iter order, but it seems nobody was relying on it (contrarily to the string case).
Diffstat (limited to 'kernel/environ.ml')
| -rw-r--r-- | kernel/environ.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/kernel/environ.ml b/kernel/environ.ml index a25714d779..15db39328c 100644 --- a/kernel/environ.ml +++ b/kernel/environ.ml @@ -168,7 +168,7 @@ let no_link_info () = ref NotLinked let add_constant_key kn cb linkinfo env = let new_constants = - Constants.add kn (cb,(linkinfo, ref None)) env.env_globals.env_constants in + Cmap_env.add kn (cb,(linkinfo, ref None)) env.env_globals.env_constants in let new_globals = { env.env_globals with env_constants = new_constants } in @@ -206,7 +206,7 @@ let evaluable_constant cst env = let lookup_mind = lookup_mind let add_mind_key kn mind_key env = - let new_inds = Inductives.add kn mind_key env.env_globals.env_inductives in + let new_inds = Mindmap_env.add kn mind_key env.env_globals.env_inductives in let new_globals = { env.env_globals with env_inductives = new_inds } in |