diff options
| author | Enrico Tassi | 2014-12-28 11:46:42 +0100 |
|---|---|---|
| committer | Enrico Tassi | 2014-12-28 11:46:42 +0100 |
| commit | 5196c281298a3168b84f1df26b71f07c873f4b5d (patch) | |
| tree | 2f291f2bc6876307024369e790f87c3d2b6ea4d6 /toplevel | |
| 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 'toplevel')
| -rw-r--r-- | toplevel/vernacentries.ml | 7 |
1 files changed, 6 insertions, 1 deletions
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index 4dc9ea4b20..0ac0a97b35 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 *) |