diff options
Diffstat (limited to 'toplevel')
-rw-r--r-- | toplevel/vernacentries.ml | 18 |
1 files changed, 14 insertions, 4 deletions
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index 0ac0a97b3..3d2052c3b 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -847,17 +847,27 @@ let vernac_set_end_tac tac = (* TO DO verifier s'il faut pas mettre exist s | TacId s ici*) let vernac_set_used_variables e = + let env = Global.env () in let tys = List.map snd (Proof.initial_goals (Proof_global.give_me_the_proof ())) in - let l = Proof_using.process_expr (Global.env ()) e tys in - let vars = Environ.named_context (Global.env ()) in + let l = Proof_using.process_expr env e tys in + let vars = Environ.named_context env in List.iter (fun id -> if not (List.exists (fun (id',_,_) -> Id.equal id id') vars) then error ("Unknown variable: " ^ Id.to_string id)) 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 + let closure_l = List.fold_right Id.Set.add closure_l Id.Set.empty in + let vars_of = Environ.global_vars_set in + let aux env entry (all_safe,rest as orig) = + match entry with + | (x,None,_) -> + if Id.Set.mem x all_safe then orig else (all_safe, (Loc.ghost,x)::rest) + | (x,Some bo, ty) -> + let vars = Id.Set.union (vars_of env bo) (vars_of env ty) in + if Id.Set.subset vars all_safe then (Id.Set.add x all_safe, rest) + else (all_safe, (Loc.ghost,x) :: rest) in + let _,to_clear = Environ.fold_named_context aux env ~init:(closure_l,[]) in vernac_solve SelectAll None Tacexpr.(TacAtom (Loc.ghost,TacClear(false,to_clear))) false |