diff options
| author | Pierre-Marie Pédrot | 2017-06-15 16:41:09 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2017-06-16 10:27:47 +0200 |
| commit | 0437339ccac602d692b5b8c071b77ac756805520 (patch) | |
| tree | 755ba115f30cd91d067250468e5946dd1a0f4dc4 /API/API.ml | |
| parent | 4f6fd16c06b9e11bc2619a34c1629bd71aba76de (diff) | |
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.
Diffstat (limited to 'API/API.ml')
| -rw-r--r-- | API/API.ml | 13 |
1 files changed, 0 insertions, 13 deletions
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 |