diff options
author | 2016-12-27 16:53:30 +0100 | |
---|---|---|
committer | 2016-12-27 18:33:25 +0100 | |
commit | 1b92c226e563643da187b8614d5888dc4855eb43 (patch) | |
tree | c4c3d204b36468b58cb71050ba95f06b8dd7bc2e /library/keys.ml | |
parent | 7c9b0a702976078b813e6493c1284af62a3f093c (diff) |
Imported Upstream version 8.6
Diffstat (limited to 'library/keys.ml')
-rw-r--r-- | library/keys.ml | 28 |
1 files changed, 10 insertions, 18 deletions
diff --git a/library/keys.ml b/library/keys.ml index 0c167494..057dc3b6 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 @@ -62,8 +58,6 @@ module Keyset = Keymap.Set (* Mapping structure for references to be considered equivalent *) -type keys = Keyset.t Keymap.t - let keys = Summary.ref Keymap.empty ~name:"Keys_decl" let add_kv k v m = @@ -153,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) |