aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel/pre_env.ml
diff options
context:
space:
mode:
Diffstat (limited to 'kernel/pre_env.ml')
-rw-r--r--kernel/pre_env.ml6
1 files changed, 3 insertions, 3 deletions
diff --git a/kernel/pre_env.ml b/kernel/pre_env.ml
index 207a37f97..2a467ad0a 100644
--- a/kernel/pre_env.ml
+++ b/kernel/pre_env.ml
@@ -39,12 +39,12 @@ type stratification = {
}
type val_kind =
- | VKvalue of values * Idset.t
+ | VKvalue of values * Id.Set.t
| VKnone
type lazy_val = val_kind ref
-type named_vals = (identifier * lazy_val) list
+type named_vals = (Id.t * lazy_val) list
type env = {
env_globals : globals;
@@ -116,7 +116,7 @@ let push_named d env =
env_named_vals = (id,rval):: env.env_named_vals }
let lookup_named_val id env =
- snd(List.find (fun (id',_) -> id_eq id id') env.env_named_vals)
+ snd(List.find (fun (id',_) -> Id.equal id id') env.env_named_vals)
(* Warning all the names should be different *)
let env_of_named id env = env