diff options
| author |  Benjamin Barenblat <bbaren@debian.org> | 2019-02-02 19:29:23 -0500 |
|---|---|---|
| committer | Benjamin Barenblat <bbaren@debian.org> | 2019-02-02 19:29:23 -0500 |
| commit | 9ebf44d84754adc5b64fcf612c6816c02c80462d (patch) | |
| tree | bf5e06a28488e0e06a2f2011ff0d110e2e02f8fc /library/keys.ml | |
| parent | 9043add656177eeac1491a73d2f3ab92bec0013c (diff) | |
Imported Upstream version 8.9.0upstream/8.9.0upstream
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 |