diff options
Diffstat (limited to 'proofs/proof.mli')
| -rw-r--r-- | proofs/proof.mli | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/proofs/proof.mli b/proofs/proof.mli index d80ac79af2..12af18f408 100644 --- a/proofs/proof.mli +++ b/proofs/proof.mli @@ -129,6 +129,9 @@ val get_proof_info : proof -> Store.t val set_proof_info : Store.t -> proof -> unit +(* Sets the section variables assumed by the proof *) +val set_used_variables : Sign.section_context -> proof -> unit +val get_used_variables : proof -> Sign.section_context option (*** Endline tactic ***) |