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

(limited to 'plugins/funind/indfun.ml')

diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml
index d12aa7f425..ad04e430cd 100644
--- a/plugins/funind/indfun.ml
+++ b/plugins/funind/indfun.ml
@@ -343,7 +343,7 @@ let error_error names e =
 let generate_principle (evd:Evd.evar_map ref) pconstants on_error
     is_general do_built (fix_rec_l:(Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list) list) recdefs  interactive_proof
     (continue_proof : int -> Names.Constant.t array -> EConstr.constr array -> int ->
-      Proof_type.tactic) : unit =
+      Tacmach.tactic) : unit =
   let names = List.map (function (((_, name),_),_,_,_,_),_ -> name) fix_rec_l in
   let fun_bodies = List.map2 prepare_body fix_rec_l recdefs in
   let funs_args = List.map fst fun_bodies in
@@ -446,7 +446,7 @@ let register_struct is_rec (fixpoint_exprl:(Vernacexpr.fixpoint_expr * Vernacexp
 
 let generate_correction_proof_wf f_ref tcc_lemma_ref
     is_mes functional_ref eq_ref rec_arg_num rec_arg_type nb_args relation
-    (_: int) (_:Names.Constant.t array) (_:EConstr.constr array) (_:int) : Proof_type.tactic =
+    (_: int) (_:Names.Constant.t array) (_:EConstr.constr array) (_:int) : Tacmach.tactic =
   Functional_principles_proofs.prove_principle_for_gen
     (f_ref,functional_ref,eq_ref)
     tcc_lemma_ref is_mes  rec_arg_num rec_arg_type relation
-- 
cgit v1.2.3