From d83e95cce852c5471593a27d0fdca39a262c885f Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Wed, 20 May 2020 00:47:21 +0200
Subject: [declare] [api] Removal of deprecated functions

The previous refactoring in `Declare` to add `CInfo.t` makes this a
good moment to clean overlays up w.r.t. deprecation.

All cases but one is just a matter of simple renaming, for the other
the use of an internal API is replaced by newer API.
---
 dev/base_include | 2 --
 1 file changed, 2 deletions(-)

(limited to 'dev')

diff --git a/dev/base_include b/dev/base_include
index efbd156758..67ea3a1fa1 100644
--- a/dev/base_include
+++ b/dev/base_include
@@ -111,10 +111,8 @@ open Search
 open Evar_refiner
 open Goal
 open Logic
-open Pfedit
 open Proof
 open Proof_using
-open Proof_global
 open Redexpr
 open Refiner
 open Tacmach
-- 
cgit v1.2.3