From f610068823b33bdc0af752a646df05b98489d7ce Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Sun, 11 Jun 2017 06:08:02 +0200
Subject: [proof] Deprecate redundant wrappers.

As we would like to reduce the role of proof_global in future
versions, we start to deprecate old compatibility aliases in `Pfedit`
in favor of the real functions underlying the 8.5 proof engine.

We also deprecate a couple of alias types and explicitly mark the few
remaining uses of `Pfedit`.
---
 vernac/command.mli | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

(limited to 'vernac/command.mli')

diff --git a/vernac/command.mli b/vernac/command.mli
index 9bbc2fdac1..2a52d9bcb5 100644
--- a/vernac/command.mli
+++ b/vernac/command.mli
@@ -15,7 +15,6 @@ open Vernacexpr
 open Constrexpr
 open Decl_kinds
 open Redexpr
-open Pfedit
 
 (** This file is about the interpretation of raw commands into typed
     ones and top-level declaration of the main Gallina objects *)
@@ -151,7 +150,7 @@ val declare_fixpoint :
   locality -> polymorphic ->
   recursive_preentry * lident list option * Evd.evar_universe_context * 
   (Context.Rel.t * Impargs.manual_implicits * int option) list ->
-  lemma_possible_guards -> decl_notation list -> unit
+  Proof_global.lemma_possible_guards -> decl_notation list -> unit
 
 val declare_cofixpoint : locality -> polymorphic -> 
   recursive_preentry * lident list option * Evd.evar_universe_context * 
-- 
cgit v1.2.3