From 118d24281bc62bb7ff503abee56f156545eb9eea Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Sat, 10 Mar 2018 23:54:14 +0100
Subject: [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.
---
 pretyping/coercion.ml        | 1 +
 pretyping/constr_matching.ml | 1 +
 pretyping/detyping.ml        | 1 +
 pretyping/glob_ops.ml        | 1 +
 pretyping/pretyping.ml       | 1 +
 pretyping/tacred.ml          | 2 +-
 pretyping/typing.ml          | 1 +
 7 files changed, 7 insertions(+), 1 deletion(-)

(limited to 'pretyping')

diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml
index c9c2445a73..bf9e37aa74 100644
--- a/pretyping/coercion.ml
+++ b/pretyping/coercion.ml
@@ -20,6 +20,7 @@ open CErrors
 open Util
 open Names
 open Term
+open Constr
 open Environ
 open EConstr
 open Vars
diff --git a/pretyping/constr_matching.ml b/pretyping/constr_matching.ml
index 0ff6a330f6..22da5315f1 100644
--- a/pretyping/constr_matching.ml
+++ b/pretyping/constr_matching.ml
@@ -13,6 +13,7 @@ open Pp
 open CErrors
 open Util
 open Names
+open Constr
 open Globnames
 open Termops
 open Term
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index fc398df9aa..e6cfe1f76a 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -14,6 +14,7 @@ open Pp
 open CErrors
 open Util
 open Names
+open Constr
 open Term
 open EConstr
 open Vars
diff --git a/pretyping/glob_ops.ml b/pretyping/glob_ops.ml
index 5056c0457e..63618c9183 100644
--- a/pretyping/glob_ops.ml
+++ b/pretyping/glob_ops.ml
@@ -11,6 +11,7 @@
 open Util
 open CAst
 open Names
+open Constr
 open Nameops
 open Globnames
 open Misctypes
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index de72f94272..92f87ab95a 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -28,6 +28,7 @@ open CErrors
 open Util
 open Names
 open Evd
+open Constr
 open Term
 open Termops
 open Environ
diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml
index 5a47acd22e..40c4cfaa45 100644
--- a/pretyping/tacred.ml
+++ b/pretyping/tacred.ml
@@ -12,7 +12,7 @@ open Pp
 open CErrors
 open Util
 open Names
-open Term
+open Constr
 open Libnames
 open Globnames
 open Termops
diff --git a/pretyping/typing.ml b/pretyping/typing.ml
index 68f9610d18..bffe36eea3 100644
--- a/pretyping/typing.ml
+++ b/pretyping/typing.ml
@@ -14,6 +14,7 @@ open Pp
 open CErrors
 open Util
 open Term
+open Constr
 open Environ
 open EConstr
 open Vars
-- 
cgit v1.2.3