Removing the now useless field env_named_val from named_context_val.

This field was only used by the VM before, but since the previous patches,
this part of the code relies on the map instead.

4 files changed, 6 insertions, 16 deletions

diff --git a/kernel/environ.ml b/kernel/environ.ml
index f4a3312ef..96e35610c 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -100,7 +100,6 @@ let fold_rel_context f env ~init =
 (* Named context *)
 
 let named_context_of_val c = c.env_named_ctx
-let named_vals_of_val c = c.env_named_val
 
 (* [map_named_val f ctxt] apply [f] to the body and the type of
    each declarations.
diff --git a/kernel/environ.mli b/kernel/environ.mli
index cb4a94d45..235ba2fd1 100644
--- a/kernel/environ.mli
+++ b/kernel/environ.mli
@@ -78,7 +78,6 @@ val fold_rel_context :
 (** {5 Context of variables (section variables and goal assumptions) } *)
 
 val named_context_of_val : named_context_val -> Context.Named.t
-val named_vals_of_val : named_context_val -> Pre_env.named_vals
 val val_of_named_context : Context.Named.t -> named_context_val
 val empty_named_context_val : named_context_val
 
diff --git a/kernel/pre_env.ml b/kernel/pre_env.ml
index defc0afc8..104fe59d1 100644
--- a/kernel/pre_env.ml
+++ b/kernel/pre_env.ml
@@ -61,11 +61,8 @@ let force_lazy_val vk = match !vk with
 let dummy_lazy_val () = ref VKnone
 let build_lazy_val vk key = vk := VKvalue (CEphemeron.create key)
 
-type named_vals = (Id.t * lazy_val) list
-
 type named_context_val = {
   env_named_ctx : Context.Named.t;
-  env_named_val : named_vals;
   env_named_map : (Context.Named.Declaration.t * lazy_val) Id.Map.t;
 }
 
@@ -84,7 +81,6 @@ type env = {
 
 let empty_named_context_val = {
   env_named_ctx = [];
-  env_named_val = [];
   env_named_map = Id.Map.empty;
 }
 
@@ -135,20 +131,19 @@ let push_named_context_val_val d rval ctxt =
 (*   assert (not (Id.Map.mem (get_id d) ctxt.env_named_map)); *)
   {
     env_named_ctx = Context.Named.add d ctxt.env_named_ctx;
-    env_named_val = (get_id d, rval) :: ctxt.env_named_val;
     env_named_map = Id.Map.add (get_id d) (d, rval) ctxt.env_named_map;
   }
 
 let push_named_context_val d ctxt =
   push_named_context_val_val d (ref VKnone) ctxt
 
-let match_named_context_val c = match c.env_named_ctx, c.env_named_val with
-| [], [] -> None
-| decl :: ctx, (_, v) :: vls ->
+let match_named_context_val c = match c.env_named_ctx with
+| [] -> None
+| decl :: ctx ->
+  let (_, v) = Id.Map.find (get_id decl) c.env_named_map in
   let map = Id.Map.remove (get_id decl) c.env_named_map in
-  let cval = { env_named_ctx = ctx; env_named_val = vls; env_named_map = map } in
+  let cval = { env_named_ctx = ctx; env_named_map = map } in
   Some (decl, v, cval)
-| _ -> assert false
 
 let map_named_val f ctxt =
   let open Context.Named.Declaration in
@@ -161,7 +156,7 @@ let map_named_val f ctxt =
     (accu, d')
   in
   let map, ctx = List.fold_map fold ctxt.env_named_map ctxt.env_named_ctx in
-  { ctxt with env_named_ctx = ctx; env_named_map = map }
+  { env_named_ctx = ctx; env_named_map = map }
 
 let push_named d env =
 (*  if not (env.env_rel_context = []) then raise (ASSERT env.env_rel_context);
diff --git a/kernel/pre_env.mli b/kernel/pre_env.mli
index 4390177da..1e4eff3d5 100644
--- a/kernel/pre_env.mli
+++ b/kernel/pre_env.mli
@@ -40,11 +40,8 @@ val force_lazy_val : lazy_val -> (values * Id.Set.t) option
 val dummy_lazy_val : unit -> lazy_val
 val build_lazy_val : lazy_val -> (values * Id.Set.t) -> unit
 
-type named_vals = (Id.t * lazy_val) list
-
 type named_context_val = private {
   env_named_ctx : Context.Named.t;
-  env_named_val : named_vals;
   env_named_map : (Context.Named.Declaration.t * lazy_val) Id.Map.t;
 }