From afceace455a4b37ced7e29175ca3424996195f7b Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Tue, 14 Nov 2017 22:36:47 +0100 Subject: [api] Rename `global_reference` to `GlobRef.t` to follow kernel style. In #6092, `global_reference` was moved to `kernel`. It makes sense to go further and use the current kernel style for names. This has a good effect on the dependency graph, as some core modules don't depend on library anymore. A question about providing equality for the GloRef module remains, as there are two different notions of equality for constants. In that sense, `KerPair` seems suspicious and at some point it should be looked at. --- library/keys.ml | 7 ++++--- 1 file changed, 4 insertions(+), 3 deletions(-) (limited to 'library/keys.ml') diff --git a/library/keys.ml b/library/keys.ml index 34a6adabe..89363455d 100644 --- a/library/keys.ml +++ b/library/keys.ml @@ -10,12 +10,13 @@ (** Keys for unification and indexing *) -open Globnames +open Names open Term +open Globnames open Libobject type key = - | KGlob of global_reference + | KGlob of GlobRef.t | KLam | KLet | KProd @@ -126,7 +127,7 @@ let constr_key kind c = | Construct (c,u) -> KGlob (ConstructRef c) | Var id -> KGlob (VarRef id) | App (f, _) -> aux f - | Proj (p, _) -> KGlob (ConstRef (Names.Projection.constant p)) + | Proj (p, _) -> KGlob (ConstRef (Projection.constant p)) | Cast (p, _, _) -> aux p | Lambda _ -> KLam | Prod _ -> KProd -- cgit v1.2.3