From 33249ab75f1a3b9791ee3179cf7ccea015ed4057 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Fri, 7 Sep 2018 13:05:46 +0200
Subject: Canonical representation of kernel substitutions.

For some reason the code was implementing substitutions as pairs of maps,
but the invariant ensured actually no observable difference between fetching
a module ident from one or the other. The split seems to be mostly due to
historical reasons. We make this invariant static by representing substitutions
as a single map.
---
 checker/values.ml | 7 ++-----
 1 file changed, 2 insertions(+), 5 deletions(-)

(limited to 'checker/values.ml')

diff --git a/checker/values.ml b/checker/values.ml
index e1b5a949ac..801874773a 100644
--- a/checker/values.ml
+++ b/checker/values.ml
@@ -15,7 +15,7 @@
 To ensure this file is up-to-date, 'make' now compares the md5 of cic.mli
 with a copy we maintain here:
 
-MD5 f7b267579138eabf86a74d6f2a7ed794 checker/cic.mli
+MD5 a127e0c2322c7846914bbca9921309c7 checker/cic.mli
 
 *)
 
@@ -185,10 +185,7 @@ let v_resolver =
 let v_mp_resolver = v_tuple "" [|v_mp;v_resolver|]
 
 let v_subst =
-  v_tuple "substitution"
-    [|v_map v_mp v_mp_resolver;
-      v_map v_uid v_mp_resolver|]
-
+  Annot ("substitution", v_map v_mp v_mp_resolver)
 
 (** kernel/lazyconstr *)
 
-- 
cgit v1.2.3