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/indfun_common.mli | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

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

diff --git a/plugins/funind/indfun_common.mli b/plugins/funind/indfun_common.mli
index 6b40c91713..f7a9cedd73 100644
--- a/plugins/funind/indfun_common.mli
+++ b/plugins/funind/indfun_common.mli
@@ -105,7 +105,7 @@ exception ToShow of exn
 
 val is_strict_tcc : unit -> bool
 
-val h_intros: Names.Id.t list -> Proof_type.tactic
+val h_intros: Names.Id.t list -> Tacmach.tactic
 val h_id :  Names.Id.t
 val hrec_id :  Names.Id.t
 val acc_inv_id :  EConstr.constr Util.delayed
@@ -114,7 +114,7 @@ val well_founded_ltof : EConstr.constr Util.delayed
 val acc_rel : EConstr.constr Util.delayed
 val well_founded : EConstr.constr Util.delayed
 val evaluable_of_global_reference : Globnames.global_reference -> Names.evaluable_global_reference
-val list_rewrite : bool -> (EConstr.constr*bool) list -> Proof_type.tactic
+val list_rewrite : bool -> (EConstr.constr*bool) list -> Tacmach.tactic
 
 val decompose_lam_n : Evd.evar_map -> int -> EConstr.t ->
   (Names.Name.t * EConstr.t) list * EConstr.t
-- 
cgit v1.2.3