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/ssr/ssrequality.mli | 12 ++++++------
 1 file changed, 6 insertions(+), 6 deletions(-)

(limited to 'plugins/ssr/ssrequality.mli')

diff --git a/plugins/ssr/ssrequality.mli b/plugins/ssr/ssrequality.mli
index f712002c1f..f9ab5d74fe 100644
--- a/plugins/ssr/ssrequality.mli
+++ b/plugins/ssr/ssrequality.mli
@@ -25,12 +25,12 @@ val mkclr : ssrclear -> ssrdocc
 val nodocc : ssrdocc
 val noclr : ssrdocc
 
-val simpltac : Ssrast.ssrsimpl -> Proof_type.tactic
+val simpltac : Ssrast.ssrsimpl -> Tacmach.tactic
 
 val newssrcongrtac :
   int * Ssrast.ssrterm ->
   Ltac_plugin.Tacinterp.interp_sign ->
-  Proof_type.goal Evd.sigma -> Proof_type.goal list Evd.sigma
+  Goal.goal Evd.sigma -> Goal.goal list Evd.sigma
 
 
 val mk_rwarg :
@@ -45,7 +45,7 @@ val ssrinstancesofrule :
   Ltac_plugin.Tacinterp.interp_sign ->
   Ssrast.ssrdir ->
   Ssrast.ssrterm ->
-  Proof_type.goal Evd.sigma -> Proof_type.goal list Evd.sigma
+  Goal.goal Evd.sigma -> Goal.goal list Evd.sigma
 
 val ssrrewritetac :
   Ltac_plugin.Tacinterp.interp_sign ->
@@ -53,11 +53,11 @@ val ssrrewritetac :
      (((Ssrast.ssrhyps option * Ssrmatching.occ) *
          Ssrmatching.rpattern option) *
         (ssrwkind * Ssrast.ssrterm)))
-           list -> Proof_type.tactic
+           list -> Tacmach.tactic
 
-val ipat_rewrite : ssrocc -> ssrdir -> EConstr.t -> Proof_type.tactic
+val ipat_rewrite : ssrocc -> ssrdir -> EConstr.t -> Tacmach.tactic
 
 val unlocktac :
   Ltac_plugin.Tacinterp.interp_sign ->
   (Ssrmatching.occ * Ssrast.ssrterm) list ->
-  Proof_type.goal Evd.sigma -> Proof_type.goal list Evd.sigma
+  Goal.goal Evd.sigma -> Goal.goal list Evd.sigma
-- 
cgit v1.2.3