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.

4 files changed, 12 insertions, 5 deletions

diff --git a/proofs/pfedit.mli b/proofs/pfedit.mli
index 31e3d506b8..b527eb3245 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 dd0e146497..07ff6e41ad 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 c2c447c92c..c9a812c4ce 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 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 *)