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. --- proofs/clenv.ml | 2 +- proofs/clenvtac.ml | 2 +- proofs/redexpr.ml | 2 +- 3 files changed, 3 insertions(+), 3 deletions(-) (limited to 'proofs') diff --git a/proofs/clenv.ml b/proofs/clenv.ml index aeaf16723..450fcddfd 100644 --- a/proofs/clenv.ml +++ b/proofs/clenv.ml @@ -13,8 +13,8 @@ open CErrors open Util open Names open Nameops -open Term open Termops +open Constr open Namegen open Environ open Evd diff --git a/proofs/clenvtac.ml b/proofs/clenvtac.ml index 209104ac3..38ed63c23 100644 --- a/proofs/clenvtac.ml +++ b/proofs/clenvtac.ml @@ -10,7 +10,7 @@ open Util open Names -open Term +open Constr open Termops open Evd open EConstr diff --git a/proofs/redexpr.ml b/proofs/redexpr.ml index a75711bae..f9e7bbfac 100644 --- a/proofs/redexpr.ml +++ b/proofs/redexpr.ml @@ -12,7 +12,7 @@ open Pp open CErrors open Util open Names -open Term +open Constr open EConstr open Declarations open Globnames -- cgit v1.2.3