aboutsummaryrefslogtreecommitdiffhomepage
path: root/API/API.ml
diff options
context:
space:
mode:
Diffstat (limited to 'API/API.ml')
-rw-r--r--API/API.ml13
1 files changed, 0 insertions, 13 deletions
diff --git a/API/API.ml b/API/API.ml
index 2b7bbd561..60703e1fa 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