aboutsummaryrefslogtreecommitdiffhomepage
path: root/library/keys.ml
diff options
context:
space:
mode:
authorGravatar Emilio Jesus Gallego Arias <e+git@x80.org>2018-03-10 23:54:14 +0100
committerGravatar Emilio Jesus Gallego Arias <e+git@x80.org>2018-05-30 17:50:37 +0200
commit118d24281bc62bb7ff503abee56f156545eb9eea (patch)
tree3b90fea811db93aedbde99d57b702e2d7f0ddb7a /library/keys.ml
parent09e0d83155e703f7b81ae9a938c165e477a56f65 (diff)
[api] Remove deprecated object from `Term`
We remove most of what was deprecated in `Term`. Now, `intf` and `kernel` are almost deprecation-free, tho I am not very convinced about the whole `Term -> Constr` renaming but I'm afraid there is no way back. Inconsistencies with the constructor policy (see #6440) remain along the code-base and I'm afraid I don't see a plan to reconcile them. The `Sorts` deprecation is hard to finalize, opening `Sorts` is not a good idea as someone added a `List` module inside it.
Diffstat (limited to 'library/keys.ml')
-rw-r--r--library/keys.ml4
1 files changed, 2 insertions, 2 deletions
diff --git a/library/keys.ml b/library/keys.ml
index 89363455d..3cadcb647 100644
--- a/library/keys.ml
+++ b/library/keys.ml
@@ -11,9 +11,9 @@
(** Keys for unification and indexing *)
open Names
-open Term
-open Globnames
+open Constr
open Libobject
+open Globnames
type key =
| KGlob of GlobRef.t