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.
---
 interp/notation_ops.ml | 1 +
 1 file changed, 1 insertion(+)

(limited to 'interp/notation_ops.ml')

diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml
index 448881dcf9..b0480aa704 100644
--- a/interp/notation_ops.ml
+++ b/interp/notation_ops.ml
@@ -13,6 +13,7 @@ open CErrors
 open Util
 open Names
 open Nameops
+open Constr
 open Globnames
 open Decl_kinds
 open Misctypes
-- 
cgit v1.2.3