Merge PR #6914: Primitive integers

Ack-by: JasonGross
Ack-by: SkySkimmer
Ack-by: ejgallego
Ack-by: gares
Ack-by: maximedenes
Ack-by: ppedrot

1 files changed, 5 insertions, 1 deletions

diff --git a/library/keys.ml b/library/keys.ml
index 58883ccc88..45b6fae2f0 100644
--- a/library/keys.ml
+++ b/library/keys.ml
@@ -25,13 +25,14 @@ type key =
   | KFix
   | KCoFix
   | KRel
+  | KInt
 
 module KeyOrdered = struct
   type t = key
 
   let hash gr =
     match gr with
-    | KGlob gr -> 8 + GlobRef.Ordered.hash gr
+    | KGlob gr -> 9 + GlobRef.Ordered.hash gr
     | KLam -> 0
     | KLet -> 1
     | KProd -> 2
@@ -40,6 +41,7 @@ module KeyOrdered = struct
     | KFix -> 5
     | KCoFix -> 6
     | KRel -> 7
+    | KInt -> 8
 
   let compare gr1 gr2 =
     match gr1, gr2 with
@@ -133,6 +135,7 @@ let constr_key kind c =
       | Evar _ -> raise Not_found
       | Sort _ -> KSort 
       | LetIn _ -> KLet
+      | Int _ -> KInt
     in Some (aux c)
   with Not_found -> None
 
@@ -148,6 +151,7 @@ let pr_key pr_global = function
   | KFix -> str"Fix"
   | KCoFix -> str"CoFix"
   | KRel -> str"Rel"
+  | KInt -> str"Int"
 
 let pr_keyset pr_global v = 
   prlist_with_sep spc (pr_key pr_global) (Keyset.elements v)