From a0e16c9e5c3f88a8b72935dd4877f13388640f69 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Thu, 12 Oct 2017 13:55:08 +0200
Subject: Make Sorts.t private

---
 engine/evarutil.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'engine/evarutil.ml')

diff --git a/engine/evarutil.ml b/engine/evarutil.ml
index 840c14b241..5c2b480db4 100644
--- a/engine/evarutil.ml
+++ b/engine/evarutil.ml
@@ -836,7 +836,7 @@ let occur_evar_upto sigma n c =
 let judge_of_new_Type evd =
   let open EConstr in
   let (evd', s) = new_univ_variable univ_rigid evd in
-  (evd', { uj_val = mkSort (Sorts.Type s); uj_type = mkSort (Sorts.Type (Univ.super s)) })
+  (evd', { uj_val = mkType s; uj_type = mkType (Univ.super s) })
 
 let subterm_source evk ?where (loc,k) =
   let evk = match k with
-- 
cgit v1.2.3


From 23f84f37c674a07e925925b7e0d50d7ee8414093 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Tue, 31 Oct 2017 17:04:02 +0100
Subject: Add relevance marks on binders.

Kernel should be mostly correct, higher levels do random stuff at
times.
---
 engine/evarutil.ml | 7 ++++---
 1 file changed, 4 insertions(+), 3 deletions(-)

(limited to 'engine/evarutil.ml')

diff --git a/engine/evarutil.ml b/engine/evarutil.ml
index 5c2b480db4..96beb72a56 100644
--- a/engine/evarutil.ml
+++ b/engine/evarutil.ml
@@ -11,6 +11,7 @@
 open CErrors
 open Util
 open Names
+open Context
 open Constr
 open Environ
 open Evd
@@ -781,13 +782,13 @@ let cached_evar_of_hyp cache sigma decl accu = match cache with
   in
   NamedDecl.fold_constr fold decl accu
 | Some cache ->
-  let id = NamedDecl.get_id decl in
+  let id = NamedDecl.get_annot decl in
   let r =
-    try Id.Map.find id cache.cache
+    try Id.Map.find id.binder_name cache.cache
     with Not_found ->
       (* Dummy value *)
       let r = ref (NamedDecl.LocalAssum (id, EConstr.mkProp), Evar.Set.empty) in
-      let () = cache.cache <- Id.Map.add id r cache.cache in
+      let () = cache.cache <- Id.Map.add id.binder_name r cache.cache in
       r
   in
   let (decl', evs) = !r in
-- 
cgit v1.2.3