diff options
Diffstat (limited to 'library/keys.ml')
| -rw-r--r-- | library/keys.ml | 9 |
1 files changed, 5 insertions, 4 deletions
diff --git a/library/keys.ml b/library/keys.ml index 34a6adab..3cadcb64 100644 --- a/library/keys.ml +++ b/library/keys.ml @@ -10,12 +10,13 @@ (** Keys for unification and indexing *) -open Globnames -open Term +open Names +open Constr open Libobject +open Globnames 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 |