From 8076de05c67a4dabc99233d8e2b81809c28794e4 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Mon, 13 Jul 2020 14:55:28 +0200
Subject: Store the default instance in named_context_val.

This is not pretty but I do not see how to do this in a way that is both
backwards compatible and efficient.
---
 kernel/environ.ml  | 7 +++++--
 kernel/environ.mli | 1 +
 2 files changed, 6 insertions(+), 2 deletions(-)

(limited to 'kernel')

diff --git a/kernel/environ.ml b/kernel/environ.ml
index e75ccbb252..03c9cb4be6 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -87,6 +87,7 @@ let build_lazy_val vk key = vk := VKvalue (CEphemeron.create key)
 type named_context_val = {
   env_named_ctx : Constr.named_context;
   env_named_map : (Constr.named_declaration * lazy_val) Id.Map.t;
+  env_named_var : Constr.t list;
 }
 
 type rel_context_val = {
@@ -109,6 +110,7 @@ type env = {
 let empty_named_context_val = {
   env_named_ctx = [];
   env_named_map = Id.Map.empty;
+  env_named_var = [];
 }
 
 let empty_rel_context_val = {
@@ -183,6 +185,7 @@ let push_named_context_val_val d rval ctxt =
   {
     env_named_ctx = Context.Named.add d ctxt.env_named_ctx;
     env_named_map = Id.Map.add (NamedDecl.get_id d) (d, rval) ctxt.env_named_map;
+    env_named_var = mkVar (NamedDecl.get_id d) :: ctxt.env_named_var;
   }
 
 let push_named_context_val d ctxt =
@@ -193,7 +196,7 @@ let match_named_context_val c = match c.env_named_ctx with
 | decl :: ctx ->
   let (_, v) = Id.Map.find (NamedDecl.get_id decl) c.env_named_map in
   let map = Id.Map.remove (NamedDecl.get_id decl) c.env_named_map in
-  let cval = { env_named_ctx = ctx; env_named_map = map } in
+  let cval = { env_named_ctx = ctx; env_named_map = map; env_named_var = List.tl c.env_named_var } in
   Some (decl, v, cval)
 
 let map_named_val f ctxt =
@@ -208,7 +211,7 @@ let map_named_val f ctxt =
   in
   let map, ctx = List.fold_left_map fold ctxt.env_named_map ctxt.env_named_ctx in
   if map == ctxt.env_named_map then ctxt
-  else { env_named_ctx = ctx; env_named_map = map }
+  else { env_named_ctx = ctx; env_named_map = map; env_named_var = ctxt.env_named_var }
 
 let push_named d env =
   {env with env_named_context = push_named_context_val d env.env_named_context}
diff --git a/kernel/environ.mli b/kernel/environ.mli
index 5cb56a2a29..55df27a8b3 100644
--- a/kernel/environ.mli
+++ b/kernel/environ.mli
@@ -69,6 +69,7 @@ type stratification = {
 type named_context_val = private {
   env_named_ctx : Constr.named_context;
   env_named_map : (Constr.named_declaration * lazy_val) Id.Map.t;
+  env_named_var : Constr.t list;
 }
 
 type rel_context_val = private {
-- 
cgit v1.2.3


From 2edad4e3903ee77155f8b164c6cf6df49c897a27 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Thu, 6 Aug 2020 12:37:22 +0200
Subject: Add a few comments about the code.

---
 kernel/environ.mli | 4 ++++
 1 file changed, 4 insertions(+)

(limited to 'kernel')

diff --git a/kernel/environ.mli b/kernel/environ.mli
index 55df27a8b3..974e794c6b 100644
--- a/kernel/environ.mli
+++ b/kernel/environ.mli
@@ -69,7 +69,11 @@ type stratification = {
 type named_context_val = private {
   env_named_ctx : Constr.named_context;
   env_named_map : (Constr.named_declaration * lazy_val) Id.Map.t;
+  (** Identifier-indexed version of [env_named_ctx] *)
   env_named_var : Constr.t list;
+  (** List of identifiers in [env_named_ctx], in the same order, including
+      let-ins. This is not used in the kernel, but is critical to preserve
+      sharing of evar instances in the proof engine. *)
 }
 
 type rel_context_val = private {
-- 
cgit v1.2.3