diff options
Diffstat (limited to 'proofs/proof.mli')
| -rw-r--r-- | proofs/proof.mli | 3 |
1 files changed, 1 insertions, 2 deletions
diff --git a/proofs/proof.mli b/proofs/proof.mli index 70615e09e..fa6007061 100644 --- a/proofs/proof.mli +++ b/proofs/proof.mli @@ -61,8 +61,7 @@ val partial_proof : proof -> Term.constr list Raises [HasUnresolvedEvar] if some evars have been left undefined. *) exception UnfinishedProof exception HasUnresolvedEvar -val return : - proof -> Term.constr -> Term.constr * Declareops.side_effects +val return : proof -> Evd.evar_map (*** Focusing actions ***) |