From 5196c281298a3168b84f1df26b71f07c873f4b5d Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Sun, 28 Dec 2014 11:46:42 +0100 Subject: Proof using: call "clear" to remove from sight the vars not selected As discussed on coqdev, clear is not perfect, Hints for trivial using cleared section vars are still used. But it is better than nothing I guess. --- proofs/proof_global.mli | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) (limited to 'proofs/proof_global.mli') diff --git a/proofs/proof_global.mli b/proofs/proof_global.mli index c2c447c92..c9a812c4c 100644 --- a/proofs/proof_global.mli +++ b/proofs/proof_global.mli @@ -126,8 +126,9 @@ val set_interp_tac : (Tacexpr.raw_tactic_expr -> unit Proofview.tactic) -> unit -(** Sets the section variables assumed by the proof *) -val set_used_variables : Names.Id.t list -> unit +(** Sets the section variables assumed by the proof, returns its closure + * (w.r.t. type dependencies *) +val set_used_variables : Names.Id.t list -> Context.section_context val get_used_variables : unit -> Context.section_context option (**********************************************************) -- cgit v1.2.3