diff options
| author | Maxime Dénès | 2017-06-20 08:09:00 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2017-06-20 08:09:00 +0200 |
| commit | 25cd7acea0df79fcc07274e429c9839de1246611 (patch) | |
| tree | 1ee95df49ec9ea7152afed41df425ea4e4760736 /API/API.ml | |
| parent | c7ac5dc8036623a02ab4ad6d11469e040e78c004 (diff) | |
| parent | 0437339ccac602d692b5b8c071b77ac756805520 (diff) | |
Merge PR#803: Clean ssr
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 515b152e42..29aa1b7a57 100644 --- a/API/API.ml +++ b/API/API.ml @@ -201,16 +201,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 |