diff options
| author |  Guillaume Melquiond <guillaume.melquiond@inria.fr> | 2016-01-02 17:05:56 +0100 |
|---|---|---|
| committer | Guillaume Melquiond <guillaume.melquiond@inria.fr> | 2016-01-02 17:05:56 +0100 |
| commit | 3f91296b5cf1dc9097d5368c2df5c6f70a04210c (patch) | |
| tree | 372c38b6ced6baadb1edf5b2f27457c05c8467e1 /library/keys.ml | |
| parent | 74c29764359272b29af081b30762549777ae8825 (diff) | |
Remove keys for evar and meta, since they cannot occur.
Diffstat (limited to 'library/keys.ml')
| -rw-r--r-- | library/keys.ml | 26 |
1 files 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) |