diff options
Diffstat (limited to 'proofs/proofview.mli')
| -rw-r--r-- | proofs/proofview.mli | 9 |
1 files changed, 4 insertions, 5 deletions
diff --git a/proofs/proofview.mli b/proofs/proofview.mli index ff327ab3b..2869e75e1 100644 --- a/proofs/proofview.mli +++ b/proofs/proofview.mli @@ -44,8 +44,11 @@ val init : (Environ.env * Term.types) list -> proofview val finished : proofview -> bool (* Returns the current value of the proofview partial proofs. *) -val return : proofview -> (constr*types) list +val return : proofview -> constr -> constr * Declareops.side_effects +val partial_proof : proofview -> constr list +val initial_goals : proofview -> (constr * types) list +val emit_side_effects : Declareops.side_effects -> proofview -> proofview (*** Focusing operations ***) @@ -181,10 +184,6 @@ val tclSENSITIVE : Goal.subgoals Goal.sensitive -> unit tactic val in_proofview : proofview -> (Evd.evar_map -> 'a) -> 'a - - - - (* Notations for building tactics. *) module Notations : sig (* Goal.bind *) |