From 0437339ccac602d692b5b8c071b77ac756805520 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Thu, 15 Jun 2017 16:41:09 +0200
Subject: Removing Proof_type from the API.

Unluckily, this forces replacing a lot of code in plugins, because the API
defined the type of goals and tactics in Proof_type, and by the no-alias rule,
this was the only one. But Proof_type was already implicitly deprecated, so
that the API should have relied on Tacmach instead.
---
 plugins/funind/recdef.mli | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'plugins/funind/recdef.mli')

diff --git a/plugins/funind/recdef.mli b/plugins/funind/recdef.mli
index e1a072799e..f3d5e73320 100644
--- a/plugins/funind/recdef.mli
+++ b/plugins/funind/recdef.mli
@@ -2,10 +2,10 @@ open API
 
 (* val evaluable_of_global_reference : Libnames.global_reference -> Names.evaluable_global_reference *)
 val tclUSER_if_not_mes : 
-  Proof_type.tactic ->
+  Tacmach.tactic ->
   bool -> 
   Names.Id.t list option -> 
-  Proof_type.tactic
+  Tacmach.tactic
 val recursive_definition :  
 bool ->
            Names.Id.t ->
-- 
cgit v1.2.3