[api] Move `Keys` to pretyping

This file is unrelated to library, but to pretyping/unification.

This commit, along with others already submitted go towards the goal
of `library` containing only the handling of library objects.

4 files changed, 9 insertions, 9 deletions

diff --git a/library/library.mllib b/library/library.mllib
index 35af5fa43b..84937ede93 100644
--- a/library/library.mllib
+++ b/library/library.mllib
@@ -11,5 +11,4 @@ Library
 States
 Kindops
 Goptions
-Keys
 Coqlib
diff --git a/library/keys.ml b/pretyping/keys.ml
index 9964992433..f8eecd80d4 100644
--- a/library/keys.ml
+++ b/pretyping/keys.ml
@@ -49,7 +49,7 @@ module KeyOrdered = struct
     | _, KGlob _ -> -1
     | KGlob _, _ -> 1
     | k, k' -> Int.compare (hash k) (hash k')
-    
+
   let equal k1 k2 =
     match k1, k2 with
     | KGlob gr1, KGlob gr2 -> GlobRef.Ordered.equal gr1 gr2
@@ -69,7 +69,7 @@ let add_kv k v m =
   try Keymap.modify k (fun k' vs -> Keyset.add v vs) m
   with Not_found -> Keymap.add k (Keyset.singleton v) m
 
-let add_keys k v = 
+let add_keys k v =
   keys := add_kv k v (add_kv v k !keys)
 
 let equiv_keys k k' =
@@ -85,7 +85,7 @@ let load_keys _ (_,(ref,ref')) =
 let cache_keys o =
   load_keys 1 o
 
-let subst_key subst k = 
+let subst_key subst k =
   match k with
   | KGlob gr -> KGlob (subst_global_reference subst gr)
   | _ -> k
@@ -98,7 +98,7 @@ let discharge_key = function
   | x -> Some x
 
 let discharge_keys (_,(k,k')) =
-  match discharge_key k, discharge_key k' with 
+  match discharge_key k, discharge_key k' with
   | Some x, Some y -> Some (x, y)
   | _ -> None
 
@@ -124,7 +124,7 @@ let constr_key kind c =
       | App (f, _) -> aux f
       | Proj (p, _) -> KGlob (GlobRef.ConstRef (Projection.constant p))
       | Cast (p, _, _) -> aux p
-      | Lambda _ -> KLam 
+      | Lambda _ -> KLam
       | Prod _ -> KProd
       | Case _ -> KCase
       | Fix _ -> KFix
@@ -132,7 +132,7 @@ let constr_key kind c =
       | Rel _ -> KRel
       | Meta _ -> raise Not_found
       | Evar _ -> raise Not_found
-      | Sort _ -> KSort 
+      | Sort _ -> KSort
       | LetIn _ -> KLet
       | Int _ -> KInt
     in Some (aux c)
@@ -152,10 +152,10 @@ let pr_key pr_global = function
   | KRel -> str"Rel"
   | KInt -> str"Int"
 
-let pr_keyset pr_global v = 
+let pr_keyset pr_global v =
   prlist_with_sep spc (pr_key pr_global) (Keyset.elements v)
 
-let pr_mapping pr_global k v = 
+let pr_mapping pr_global k v =
   pr_key pr_global k ++ str" <-> " ++ pr_keyset pr_global v
 
 let pr_keys pr_global =
diff --git a/library/keys.mli b/pretyping/keys.mli
index a7adf7791b..a7adf7791b 100644
--- a/library/keys.mli
+++ b/pretyping/keys.mli
diff --git a/pretyping/pretyping.mllib b/pretyping/pretyping.mllib
index 34a6cecc95..0ca39f0404 100644
--- a/pretyping/pretyping.mllib
+++ b/pretyping/pretyping.mllib
@@ -35,4 +35,5 @@ Indrec
 GlobEnv
 Cases
 Pretyping
+Keys
 Unification