diff options
| author |  Enrico Tassi <Enrico.Tassi@inria.fr> | 2014-12-28 11:46:42 +0100 |
|---|---|---|
| committer | Enrico Tassi <Enrico.Tassi@inria.fr> | 2014-12-28 11:46:42 +0100 |
| commit | 5196c281298a3168b84f1df26b71f07c873f4b5d (patch) | |
| tree | 2f291f2bc6876307024369e790f87c3d2b6ea4d6 /proofs | |
| parent | 0276f8357a2ea1d83cb6b85b86b8b3f5a1e4579d (diff) | |
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.
Diffstat (limited to 'proofs')
| -rw-r--r-- | proofs/pfedit.mli | 2 | ||||
| -rw-r--r-- | proofs/proof_global.ml | 3 | ||||
| -rw-r--r-- | proofs/proof_global.mli | 5 |
3 files changed, 6 insertions, 4 deletions
diff --git a/proofs/pfedit.mli b/proofs/pfedit.mli index 31e3d506b..b527eb324 100644 --- a/proofs/pfedit.mli +++ b/proofs/pfedit.mli @@ -117,7 +117,7 @@ val set_end_tac : Tacexpr.raw_tactic_expr -> unit (** {6 ... } *) (** [set_used_variables l] declares that section variables [l] will be used in the proof *) -val set_used_variables : Id.t list -> unit +val set_used_variables : Id.t list -> Context.section_context val get_used_variables : unit -> Context.section_context option (** {6 ... } *) diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml index dd0e14649..07ff6e41a 100644 --- a/proofs/proof_global.ml +++ b/proofs/proof_global.ml @@ -259,7 +259,8 @@ let set_used_variables l = | p :: rest -> if not (Option.is_empty p.section_vars) then Errors.error "Used section variables can be declared only once"; - pstates := { p with section_vars = Some ctx} :: rest + pstates := { p with section_vars = Some ctx} :: rest; + ctx let get_open_goals () = let gl, gll, shelf , _ , _ = Proof.proof (cur_pstate ()).proof in 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 (**********************************************************) |