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.
---
 API/API.ml | 13 -------------
 1 file changed, 13 deletions(-)

(limited to 'API/API.ml')

diff --git a/API/API.ml b/API/API.ml
index 2b7bbd561b..60703e1fa8 100644
--- a/API/API.ml
+++ b/API/API.ml
@@ -200,16 +200,3 @@ module Entries =
                            | ParameterEntry of parameter_entry
                            | ProjectionEntry of projection_entry
   end
-
-(* NOTE: It does not make sense to replace the following "module expression"
-   simply with "module Proof_type = Proof_type" because
-   there is only "proofs/proof_type.mli";
-   there is no "proofs/proof_type.ml" file *)
-module Proof_type =
-  struct
-    type goal = Goal.goal
-    type tactic = goal Evd.sigma -> goal list Evd.sigma
-    type rule = Proof_type.prim_rule =
-      | Cut of bool * bool * Names.Id.t * Term.types
-      | Refine of Term.constr
-  end
-- 
cgit v1.2.3