diff options
| -rw-r--r-- | proofs/pfedit.mli | 2 | ||||
| -rw-r--r-- | proofs/proof_global.ml | 3 | ||||
| -rw-r--r-- | proofs/proof_global.mli | 5 | ||||
| -rw-r--r-- | toplevel/vernacentries.ml | 7 |
4 files changed, 12 insertions, 5 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 (**********************************************************) diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index 4dc9ea4b2..0ac0a97b3 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -855,7 +855,12 @@ let vernac_set_used_variables e = if not (List.exists (fun (id',_,_) -> Id.equal id id') vars) then error ("Unknown variable: " ^ Id.to_string id)) l; - set_used_variables l + let closure_l = List.map pi1 (set_used_variables l) in + let to_clear = CList.map_filter (fun (x,_,_) -> + if not(List.mem x closure_l) then Some(Loc.ghost,x) else None) vars in + vernac_solve + SelectAll None Tacexpr.(TacAtom (Loc.ghost,TacClear(false,to_clear))) false + (*****************************) (* Auxiliary file management *) |