diff options
Diffstat (limited to 'proofs/tacmach.ml')
| -rw-r--r-- | proofs/tacmach.ml | 2 |
1 files changed, 0 insertions, 2 deletions
diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml index 4524fe6a1..80a450bcd 100644 --- a/proofs/tacmach.ml +++ b/proofs/tacmach.ml @@ -109,8 +109,6 @@ let pf_matches = pf_apply Matching.matches_conv (* Tactics handling a list of goals *) (************************************) -type validation_list = proof_tree list -> proof_tree list - type tactic_list = Refiner.tactic_list let first_goal = first_goal |