diff options
Diffstat (limited to 'proofs')
| -rw-r--r-- | proofs/refiner.mli | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/proofs/refiner.mli b/proofs/refiner.mli index ba092e89ef..e79534b38f 100644 --- a/proofs/refiner.mli +++ b/proofs/refiner.mli @@ -198,6 +198,7 @@ val solve_pftreestate : tactic -> pftreestate -> pftreestate val weak_undo_pftreestate : pftreestate -> pftreestate val mk_pftreestate : goal -> pftreestate +val extract_open_proof : evar_map -> proof_tree -> constr * (int * types) list val extract_open_pftreestate : pftreestate -> constr * Termops.metamap val extract_pftreestate : pftreestate -> constr val first_unproven : pftreestate -> pftreestate |