diff options
Diffstat (limited to 'proofs/refiner.mli')
| -rw-r--r-- | proofs/refiner.mli | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/proofs/refiner.mli b/proofs/refiner.mli index 4c1e2f977..47d44a9f1 100644 --- a/proofs/refiner.mli +++ b/proofs/refiner.mli @@ -117,7 +117,7 @@ val solve_pftreestate : tactic -> pftreestate -> pftreestate val weak_undo_pftreestate : pftreestate -> pftreestate val mk_pftreestate : goal -> pftreestate -val extract_open_pftreestate : pftreestate -> constr * (int * typed_type) list +val extract_open_pftreestate : pftreestate -> constr * (int * types) list val extract_pftreestate : pftreestate -> constr val first_unproven : pftreestate -> pftreestate val last_unproven : pftreestate -> pftreestate |