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 6ea71c4db..01ffae0d4 100644 --- a/proofs/refiner.mli +++ b/proofs/refiner.mli @@ -172,7 +172,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 * types) list +val extract_open_pftreestate : pftreestate -> constr * Termops.metamap val extract_pftreestate : pftreestate -> constr val first_unproven : pftreestate -> pftreestate val last_unproven : pftreestate -> pftreestate |