diff options
Diffstat (limited to 'proofs/tacmach.mli')
| -rw-r--r-- | proofs/tacmach.mli | 5 |
1 files changed, 1 insertions, 4 deletions
diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli index 0a685a447..7dda94210 100644 --- a/proofs/tacmach.mli +++ b/proofs/tacmach.mli @@ -89,7 +89,7 @@ val frontier : transformation_tactic (*s Functions for handling the state of the proof editor. *) -type pftreestate +type pftreestate = Refiner.pftreestate val proof_of_pftreestate : pftreestate -> proof_tree val cursor_of_pftreestate : pftreestate -> int list @@ -114,9 +114,6 @@ val prev_unproven : pftreestate -> pftreestate val top_of_tree : pftreestate -> pftreestate val change_constraints_pftreestate : evar_map -> pftreestate -> pftreestate -val instantiate_pf : int -> constr -> pftreestate -> pftreestate -val instantiate_pf_com : int -> Coqast.t -> pftreestate -> pftreestate - (*s Tacticals re-exported from the Refiner module. *) |