From 3f91296b5cf1dc9097d5368c2df5c6f70a04210c Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond <guillaume.melquiond@inria.fr>
Date: Sat, 2 Jan 2016 17:05:56 +0100
Subject: Remove keys for evar and meta, since they cannot occur.

---
 library/keys.ml | 26 ++++++++++----------------
 1 file changed, 10 insertions(+), 16 deletions(-)

diff --git a/library/keys.ml b/library/keys.ml
index 6b2466f3d..e30cf6717 100644
--- a/library/keys.ml
+++ b/library/keys.ml
@@ -12,35 +12,31 @@ open Globnames
 open Term
 open Libobject
 
-type key = 
+type key =
   | KGlob of global_reference
-  | KLam 
+  | KLam
   | KLet
   | KProd
   | KSort
-  | KEvar
-  | KCase 
-  | KFix 
+  | KCase
+  | KFix
   | KCoFix
-  | KRel 
-  | KMeta
+  | KRel
 
 module KeyOrdered = struct
   type t = key
 
   let hash gr =
     match gr with
-    | KGlob gr -> 10 + RefOrdered.hash gr
+    | KGlob gr -> 8 + RefOrdered.hash gr
     | KLam -> 0
     | KLet -> 1
     | KProd -> 2
     | KSort -> 3
-    | KEvar -> 4
-    | KCase -> 5
-    | KFix -> 6
-    | KCoFix -> 7
-    | KRel -> 8
-    | KMeta -> 9
+    | KCase -> 4
+    | KFix -> 5
+    | KCoFix -> 6
+    | KRel -> 7
 
   let compare gr1 gr2 =
     match gr1, gr2 with
@@ -151,12 +147,10 @@ let pr_key pr_global = function
   | KLet -> str"Let"
   | KProd -> str"Product"
   | KSort -> str"Sort"
-  | KEvar -> str"Evar"
   | KCase -> str"Case"
   | KFix -> str"Fix"
   | KCoFix -> str"CoFix"
   | KRel -> str"Rel"
-  | KMeta -> str"Meta"
 
 let pr_keyset pr_global v = 
   prlist_with_sep spc (pr_key pr_global) (Keyset.elements v)
-- 
cgit v1.2.3