Proof using: let-in policy, optional auto-clear, forward closure*

- "Proof using p*" means: use p and any section var about p.
- Simplify the grammar/parser for proof using <expression>.
- Section variables with a body (let-in) are pulled in automatically
  since they are safe to be used (add no extra quantification)
- automatic clear of "unused" section variables made optional:
    Set Proof Using Clear Unused.
  since clearing section hypotheses does not "always work" (e.g. hint
  databases are not really cleaned)
- term_typing: trigger a "suggest proof using" message also for Let
  theorems.

14 files changed, 301 insertions, 160 deletions

diff --git a/doc/refman/RefMan-pro.tex b/doc/refman/RefMan-pro.tex
index 7af87a399..5dbf31553 100644
--- a/doc/refman/RefMan-pro.tex
+++ b/doc/refman/RefMan-pro.tex
@@ -157,6 +157,14 @@ in Section~\ref{ProofWith}.
   
   Use only section variables occurring in the statement.
 
+\variant {\tt Proof using Type*.} 
+  
+  The {\tt *} operator computes the forward transitive closure.
+  E.g. if the variable {\tt H} has type {\tt p < 5} then {\tt H} is
+  in {\tt p*} since {\tt p} occurs in the type of {\tt H}.
+  {\tt Type* } is the forward transitive closure of the entire set of
+  section variables occurring in the statement.
+
 \variant {\tt Proof using -(} {\ident$_1$} {\ldots} {\ident$_n$} {\tt ).}
   
   Use all section variables except {\ident$_1$} {\ldots} {\ident$_n$}.
@@ -164,14 +172,18 @@ in Section~\ref{ProofWith}.
 \variant {\tt Proof using }  {\emph collection$_1$} {\tt + } {\emph collection$_2$} {\tt .}
 \variant {\tt Proof using }  {\emph collection$_1$} {\tt - } {\emph collection$_2$} {\tt .}
 \variant {\tt Proof using }  {\emph collection$_1$} {\tt - (} {\ident$_1$} {\ldots} {\ident$_n$} {\tt ).}
+\variant {\tt Proof using }  {\emph collection$_1$}{\tt* .}
 
-  Use section variables being in the set union or set difference of the two
-  colelctions.  See Section~\ref{Collection} to know how to form a named
+  Use section variables being, respectively, in the set union, set difference,
+  set complement, set forward transitive closure.
+  See Section~\ref{Collection} to know how to form a named
   collection.
+  The {\tt *} operator binds stronger than {\tt +} and {\tt -}.
 
 \subsubsection{{\tt Proof using} options}
-\comindex{Default Proof Using}
-\comindex{Suggest Proof Using}
+\optindex{Default Proof Using}
+\optindex{Suggest Proof Using}
+\optindex{Proof Using Clear Unused}
 
 The following options modify the behavior of {\tt Proof using}.
 
@@ -186,11 +198,17 @@ The following options modify the behavior of {\tt Proof using}.
   When {\tt Qed} is performed, suggest a {\tt using} annotation if
   the user did not provide one.
 
+\variant{\tt Unset Proof Using Clear Unused.}
+
+  When {\tt Proof using a} all section variables but for {\tt a} and
+  the variables used in the type of {\tt a} are cleared.
+  This option can be used to turn off this behavior.
+
 \subsubsection[\tt Collection]{Name a set of section hypotheses for {\tt Proof using}}
 \comindex{Collection}\label{Collection}
 
 The command {\tt Collection} can be used to name a set of section hypotheses,
-with the purpose of making {\tt Proof using} annotations more compat.
+with the purpose of making {\tt Proof using} annotations more compact.
 
 \variant {\tt Collection Some := x y z.}
 
@@ -209,7 +227,7 @@ with the purpose of making {\tt Proof using} annotations more compat.
 \variant {\tt Collection Many := Fewer - (x y).}
 
   Define the collection named "Many" containing the set difference
-  of "Fewer" and the unamed collection {\tt x y}.
+  of "Fewer" and the unnamed collection {\tt x y}.
 
 \subsection[\tt Abort.]{\tt Abort.\comindex{Abort}}
 
diff --git a/intf/vernacexpr.mli b/intf/vernacexpr.mli
index 9248fa953..fd6e1c6ae 100644
--- a/intf/vernacexpr.mli
+++ b/intf/vernacexpr.mli
@@ -225,12 +225,12 @@ type scheme =
   | EqualityScheme of reference or_by_notation
 
 type section_subset_expr =
-  | SsSet of lident list
+  | SsEmpty
+  | SsSingl of lident
   | SsCompl of section_subset_expr
   | SsUnion of section_subset_expr * section_subset_expr
   | SsSubstr of section_subset_expr * section_subset_expr
-
-type section_subset_descr = SsAll | SsType | SsExpr of section_subset_expr
+  | SsFwdClose of section_subset_expr
 
 (** Extension identifiers for the VERNAC EXTEND mechanism. *)
 type extend_name =
@@ -336,7 +336,7 @@ type vernac_expr =
       class_rawexpr * class_rawexpr
   | VernacIdentityCoercion of obsolete_locality * lident *
       class_rawexpr * class_rawexpr
-  | VernacNameSectionHypSet of lident * section_subset_descr 
+  | VernacNameSectionHypSet of lident * section_subset_expr 
 
   (* Type classes *)
   | VernacInstance of
@@ -441,7 +441,7 @@ type vernac_expr =
   | VernacEndSubproof
   | VernacShow of showable
   | VernacCheckGuard
-  | VernacProof of raw_tactic_expr option * section_subset_descr option
+  | VernacProof of raw_tactic_expr option * section_subset_expr option
   | VernacProofMode of string
   (* Toplevel control *)
   | VernacToplevelControl of exn
diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml
index 8eb920fb7..b6df8f454 100644
--- a/kernel/term_typing.ml
+++ b/kernel/term_typing.ml
@@ -182,14 +182,17 @@ let global_vars_set_constant_type env = function
 	  (fun t c -> Id.Set.union (global_vars_set env t) c))
       ctx ~init:Id.Set.empty
 
-let record_aux env s1 s2 =
+let record_aux env s_ty s_bo suggested_expr =
+  let in_ty = keep_hyps env s_ty in
   let v =
     String.concat " "
-      (List.map (fun (id, _,_) -> Id.to_string id)
-        (keep_hyps env (Id.Set.union s1 s2))) in
-  Aux_file.record_in_aux "context_used" v
+      (CList.map_filter (fun (id, _,_) ->
+          if List.exists (fun (id',_,_) -> Id.equal id id') in_ty then None
+          else Some (Id.to_string id))
+        (keep_hyps env s_bo)) in
+  Aux_file.record_in_aux "context_used" (v ^ ";" ^ suggested_expr)
 
-let suggest_proof_using = ref (fun _ _ _ _ _ -> ())
+let suggest_proof_using = ref (fun _ _ _ _ _ -> "")
 let set_suggest_proof_using f = suggest_proof_using := f
 
 let build_constant_declaration kn env (def,typ,proj,poly,univs,inline_code,ctx) =
@@ -225,15 +228,17 @@ let build_constant_declaration kn env (def,typ,proj,poly,univs,inline_code,ctx)
                 (Opaqueproof.force_proof (opaque_tables env) lc) in
             (* we force so that cst are added to the env immediately after *)
             ignore(Opaqueproof.force_constraints (opaque_tables env) lc);
-            !suggest_proof_using kn env vars ids_typ context_ids;
+            let expr =
+              !suggest_proof_using (Constant.to_string kn)
+                env vars ids_typ context_ids in
             if !Flags.compilation_mode = Flags.BuildVo then
-              record_aux env ids_typ vars;
+              record_aux env ids_typ vars expr;
             vars
         in
         keep_hyps env (Idset.union ids_typ ids_def), def
     | None ->
         if !Flags.compilation_mode = Flags.BuildVo then
-          record_aux env Id.Set.empty Id.Set.empty;
+          record_aux env Id.Set.empty Id.Set.empty "";
         [], def (* Empty section context: no need to check *)
     | Some declared ->
         (* We use the declared set and chain a check of correctness *)
@@ -307,6 +312,20 @@ let translate_local_def env id centry =
   let def,typ,proj,poly,univs,inline_code,ctx =
     infer_declaration env None (DefinitionEntry centry) in
   let typ = type_of_constant_type env typ in
+  if ctx = None && !Flags.compilation_mode = Flags.BuildVo then begin
+    match def with
+    | Undef _ -> ()
+    | Def _ -> ()
+    | OpaqueDef lc ->
+       let context_ids = List.map pi1 (named_context env) in
+       let ids_typ = global_vars_set env typ in
+       let ids_def = global_vars_set env
+         (Opaqueproof.force_proof (opaque_tables env) lc) in
+       let expr =
+         !suggest_proof_using (Id.to_string id)
+           env ids_def ids_typ context_ids in
+       record_aux env ids_typ ids_def expr
+  end;
   def, typ, univs
 
 (* Insertion of inductive types. *)
diff --git a/kernel/term_typing.mli b/kernel/term_typing.mli
index 1b54b1ea1..8d92bcc68 100644
--- a/kernel/term_typing.mli
+++ b/kernel/term_typing.mli
@@ -44,4 +44,4 @@ val build_constant_declaration :
   constant -> env -> Cooking.result -> constant_body
 
 val set_suggest_proof_using :
-  (constant -> env -> Id.Set.t -> Id.Set.t -> Id.t list -> unit) -> unit
+  (string -> env -> Id.Set.t -> Id.Set.t -> Id.t list -> string) -> unit
diff --git a/parsing/g_proofs.ml4 b/parsing/g_proofs.ml4
index 1e254c16b..7f5459bfa 100644
--- a/parsing/g_proofs.ml4
+++ b/parsing/g_proofs.ml4
@@ -37,12 +37,12 @@ GEXTEND Gram
   command:
     [ [ IDENT "Goal"; c = lconstr -> VernacGoal c
       | IDENT "Proof" ->
-          VernacProof (None,hint_proof_using G_vernac.section_subset_descr None)
+          VernacProof (None,hint_proof_using G_vernac.section_subset_expr None)
       | IDENT "Proof" ; IDENT "Mode" ; mn = string -> VernacProofMode mn
       | IDENT "Proof"; "with"; ta = tactic; 
-        l = OPT [ "using"; l = G_vernac.section_subset_descr -> l ] ->
-          VernacProof (Some ta,hint_proof_using G_vernac.section_subset_descr l)
-      | IDENT "Proof"; "using"; l = G_vernac.section_subset_descr;
+        l = OPT [ "using"; l = G_vernac.section_subset_expr -> l ] ->
+          VernacProof (Some ta,hint_proof_using G_vernac.section_subset_expr l)
+      | IDENT "Proof"; "using"; l = G_vernac.section_subset_expr;
         ta = OPT [ "with"; ta = tactic -> ta ] ->
           VernacProof (ta,Some l)
       | IDENT "Proof"; c = lconstr -> VernacExactProof c
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index e9915fceb..fc0a4c8c3 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -46,7 +46,7 @@ let record_field = Gram.entry_create "vernac:record_field"
 let of_type_with_opt_coercion = Gram.entry_create "vernac:of_type_with_opt_coercion"
 let subgoal_command = Gram.entry_create "proof_mode:subgoal_command"
 let instance_name = Gram.entry_create "vernac:instance_name"
-let section_subset_descr = Gram.entry_create "vernac:section_subset_descr"
+let section_subset_expr = Gram.entry_create "vernac:section_subset_expr"
 
 let command_entry = ref noedit_mode
 let set_command_entry e = command_entry := e
@@ -447,20 +447,24 @@ GEXTEND Gram
   ;
 END
 
-let only_identrefs =
-  Gram.Entry.of_parser "test_only_identrefs"
+let only_starredidentrefs =
+  Gram.Entry.of_parser "test_only_starredidentrefs"
     (fun strm ->
       let rec aux n =
       match get_tok (Util.stream_nth n strm) with
         | KEYWORD "." -> ()
         | KEYWORD ")" -> ()
-        | IDENT _ -> aux (n+1)
+        | (IDENT _ | KEYWORD "Type" | KEYWORD "*") -> aux (n+1)
         | _ -> raise Stream.Failure in
       aux 0)
+let starredidentreflist_to_expr l =
+  match l with
+  | [] -> SsEmpty
+  | x :: xs -> List.fold_right (fun i acc -> SsUnion(i,acc)) xs x
 
 (* Modules and Sections *)
 GEXTEND Gram
-  GLOBAL: gallina_ext module_expr module_type section_subset_descr;
+  GLOBAL: gallina_ext module_expr module_type section_subset_expr;
 
   gallina_ext:
     [ [ (* Interactive module declaration *)
@@ -483,7 +487,7 @@ GEXTEND Gram
       | IDENT "End"; id = identref -> VernacEndSegment id
 
       (* Naming a set of section hyps *)
-      | IDENT "Collection"; id = identref; ":="; expr = section_subset_descr ->
+      | IDENT "Collection"; id = identref; ":="; expr = section_subset_expr ->
           VernacNameSectionHypSet (id, expr)
 
       (* Requiring an already compiled module *)
@@ -574,22 +578,32 @@ GEXTEND Gram
           CMwith (!@loc,mty,decl)
       ] ]
   ;
-  section_subset_descr:
-    [ [ IDENT "All" -> SsAll
-      | "Type" -> SsType
-      | only_identrefs; l = LIST0 identref -> SsExpr (SsSet l)
-      | e = section_subset_expr -> SsExpr e ] ]
-  ;
+  (* Proof using *)
   section_subset_expr:
+    [ [ only_starredidentrefs; l = LIST0 starredidentref ->
+          starredidentreflist_to_expr l
+      | e = ssexpr -> e ]]
+  ;
+  starredidentref:
+    [ [ i = identref -> SsSingl i
+      | i = identref; "*" -> SsFwdClose(SsSingl i)
+      | "Type" -> SsSingl (!@loc, Id.of_string "Type")
+      | "Type"; "*" -> SsFwdClose (SsSingl (!@loc, Id.of_string "Type")) ]]
+  ;
+  ssexpr:
     [ "35" 
-      [ "-"; e = section_subset_expr -> SsCompl e ]
+      [ "-"; e = ssexpr -> SsCompl e ]
     | "50"
-      [ e1 = section_subset_expr; "-"; e2 = section_subset_expr->SsSubstr(e1,e2)
-      | e1 = section_subset_expr; "+"; e2 = section_subset_expr->SsUnion(e1,e2)]
+      [ e1 = ssexpr; "-"; e2 = ssexpr->SsSubstr(e1,e2)
+      | e1 = ssexpr; "+"; e2 = ssexpr->SsUnion(e1,e2)]
     | "0"
-      [ i = identref -> SsSet [i]
-      | "("; only_identrefs; l = LIST0 identref; ")"-> SsSet l
-      | "("; e = section_subset_expr; ")"-> e ] ]
+      [ i = starredidentref -> i
+      | "("; only_starredidentrefs; l = LIST0 starredidentref; ")"->
+          starredidentreflist_to_expr l
+      | "("; only_starredidentrefs; l = LIST0 starredidentref; ")"; "*" ->
+          SsFwdClose(starredidentreflist_to_expr l)
+      | "("; e = ssexpr; ")"-> e 
+      | "("; e = ssexpr; ")"; "*" -> SsFwdClose e ] ]
   ;
 END
 
diff --git a/proofs/pfedit.mli b/proofs/pfedit.mli
index 4aa3c3bfd..b1fba132d 100644
--- a/proofs/pfedit.mli
+++ b/proofs/pfedit.mli
@@ -117,7 +117,8 @@ 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 -> Context.section_context
+val set_used_variables :
+  Id.t list -> Context.section_context * (Loc.t * Names.Id.t) list
 val get_used_variables : unit -> Context.section_context option
 
 (** {6 ... } *)
diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml
index 254aa8f78..f777e6ed7 100644
--- a/proofs/proof_global.ml
+++ b/proofs/proof_global.ml
@@ -250,17 +250,43 @@ let start_dependent_proof id str goals terminator =
 
 let get_used_variables () = (cur_pstate ()).section_vars
 
+let proof_using_auto_clear = ref true
+let _ = Goptions.declare_bool_option
+    { Goptions.optsync  = true;
+      Goptions.optdepr  = false;
+      Goptions.optname  = "Proof using Clear Unused";
+      Goptions.optkey   = ["Proof";"Using";"Clear";"Unused"];
+      Goptions.optread  = (fun () -> !proof_using_auto_clear);
+      Goptions.optwrite = (fun b -> proof_using_auto_clear := b) }
+
 let set_used_variables l =
   let env = Global.env () in
   let ids = List.fold_right Id.Set.add l Id.Set.empty in
   let ctx = Environ.keep_hyps env ids in
+  let ctx_set =
+    List.fold_right Id.Set.add (List.map pi1 ctx) Id.Set.empty in
+  let vars_of = Environ.global_vars_set in
+  let aux env entry (ctx, all_safe, to_clear as orig) =
+    match entry with
+    | (x,None,_) ->
+       if Id.Set.mem x all_safe then orig
+       else (ctx, all_safe, (Loc.ghost,x)::to_clear) 
+    | (x,Some bo, ty) as decl ->
+       if Id.Set.mem x all_safe then orig else
+       let vars = Id.Set.union (vars_of env bo) (vars_of env ty) in
+       if Id.Set.subset vars all_safe
+       then (decl :: ctx, Id.Set.add x all_safe, to_clear)
+       else (ctx, all_safe, (Loc.ghost,x) :: to_clear) in
+  let ctx, _, to_clear =
+    Environ.fold_named_context aux env ~init:(ctx,ctx_set,[]) in
+  let to_clear = if !proof_using_auto_clear then to_clear else [] in
   match !pstates with
   | [] -> raise NoCurrentProof
   | 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;
-      ctx
+      ctx, to_clear
 
 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 b5dd5ef85..028116049 100644
--- a/proofs/proof_global.mli
+++ b/proofs/proof_global.mli
@@ -129,8 +129,10 @@ val set_interp_tac :
     -> 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
+ * (w.r.t. type dependencies and let-ins covered by it) + a list of
+ * ids to be cleared *)
+val set_used_variables :
+  Names.Id.t list -> Context.section_context * (Loc.t * Names.Id.t) list
 val get_used_variables : unit -> Context.section_context option
 
 (**********************************************************)
diff --git a/proofs/proof_using.ml b/proofs/proof_using.ml
index f66e96571..7eed1cb31 100644
--- a/proofs/proof_using.ml
+++ b/proofs/proof_using.ml
@@ -11,20 +11,15 @@ open Environ
 open Util
 open Vernacexpr
 
-let to_string = function
-  | SsAll -> "All"
-  | SsType -> "Type"
-  | SsExpr(SsSet l)-> String.concat " " (List.map Id.to_string (List.map snd l))
-  | SsExpr e ->
-      let rec aux = function
-        | SsSet [] -> "( )"
-        | SsSet [_,x] -> Id.to_string x
-        | SsSet l ->
-          "(" ^ String.concat " " (List.map Id.to_string (List.map snd l)) ^ ")"
-        | SsCompl e -> "-" ^ aux e^""
-        | SsUnion(e1,e2) -> "("^aux e1 ^" + "^ aux e2^")"
-        | SsSubstr(e1,e2) -> "("^aux e1 ^" - "^ aux e2^")"
-      in aux e
+let to_string e =
+  let rec aux = function
+    | SsEmpty -> "()"
+    | SsSingl (_,id) -> "("^Id.to_string id^")"
+    | SsCompl e -> "-" ^ aux e^""
+    | SsUnion(e1,e2) -> "("^aux e1 ^" + "^ aux e2^")"
+    | SsSubstr(e1,e2) -> "("^aux e1 ^" - "^ aux e2^")"
+    | SsFwdClose e -> "("^aux e^")*"
+  in aux e
 
 let known_names = Summary.ref [] ~name:"proofusing-nameset"
 
@@ -36,30 +31,48 @@ let in_nameset =
     discharge_function = (fun _ -> None)
   }
 
+let rec close_fwd e s =
+  let s' =
+    List.fold_left (fun s (id,b,ty) ->      
+      let vb = Option.(default Id.Set.empty (map (global_vars_set e) b)) in
+      let vty = global_vars_set e ty in
+      let vbty = Id.Set.union vb vty in
+      if Id.Set.exists (fun v -> Id.Set.mem v s) vbty
+      then Id.Set.add id (Id.Set.union s vbty) else s)
+    s (named_context e)
+    in
+  if Id.Set.equal s s' then s else close_fwd e s'
+;;
+
 let rec process_expr env e ty =
-  match e with
-  | SsAll ->
-      List.fold_right Id.Set.add (List.map pi1 (named_context env)) Id.Set.empty
-  | SsExpr e ->
-      let rec aux = function
-        | SsSet l -> set_of_list env (List.map snd l)
-        | SsUnion(e1,e2) -> Id.Set.union (aux e1) (aux e2)
-        | SsSubstr(e1,e2) -> Id.Set.diff (aux e1) (aux e2)
-        | SsCompl e -> Id.Set.diff (full_set env) (aux e)
-      in
-        aux e
-  | SsType ->
-      List.fold_left (fun acc ty ->
+  let rec aux = function
+    | SsEmpty -> Id.Set.empty
+    | SsSingl (_,id) -> set_of_id env ty id
+    | SsUnion(e1,e2) -> Id.Set.union (aux e1) (aux e2)
+    | SsSubstr(e1,e2) -> Id.Set.diff (aux e1) (aux e2)
+    | SsCompl e -> Id.Set.diff (full_set env) (aux e)
+    | SsFwdClose e -> close_fwd env (aux e)
+  in
+    aux e
+
+and set_of_id env ty id =
+  if Id.to_string id = "Type" then
+    List.fold_left (fun acc ty ->
         Id.Set.union (global_vars_set env ty) acc)
       Id.Set.empty ty
-and set_of_list env = function
-  | [x] when CList.mem_assoc_f Id.equal x !known_names ->
-      process_expr env (CList.assoc_f Id.equal x !known_names) []
-  | l -> List.fold_right Id.Set.add l Id.Set.empty
-and full_set env = set_of_list env (List.map pi1 (named_context env))
+  else if Id.to_string id = "All" then
+    List.fold_right Id.Set.add (List.map pi1 (named_context env)) Id.Set.empty
+  else if CList.mem_assoc_f Id.equal id !known_names then
+    process_expr env (CList.assoc_f Id.equal id !known_names) []
+  else Id.Set.singleton id
+
+and full_set env =
+  List.fold_right Id.Set.add (List.map pi1 (named_context env)) Id.Set.empty
 
 let process_expr env e ty =
-  let s = Id.Set.union (process_expr env SsType ty) (process_expr env e []) in
+  let ty_expr = SsSingl(Loc.ghost, Id.of_string "Type") in
+  let v_ty = process_expr env ty_expr ty in
+  let s = Id.Set.union v_ty (process_expr env e ty) in
   Id.Set.elements s
 
 let name_set id expr = Lib.add_anonymous_leaf (in_nameset (id,expr))
@@ -77,62 +90,49 @@ let minimize_hyps env ids =
   in
     aux ids
 
-let minimize_unused_hyps env ids =
-  let all_ids = List.map pi1 (named_context env) in
-  let deps_of =
-    let cache =
-      List.map (fun id -> id,really_needed env (Id.Set.singleton id)) all_ids in
-    fun id -> List.assoc id cache in
-  let inv_dep_of =
-    let cache_sum cache id stuff =
-      try Id.Map.add id (Id.Set.add stuff (Id.Map.find id cache)) cache
-      with Not_found -> Id.Map.add id (Id.Set.singleton stuff) cache in
-    let cache =
-      List.fold_left (fun cache id ->
-        Id.Set.fold (fun d cache -> cache_sum cache d id)
-          (Id.Set.remove id (deps_of id)) cache)
-        Id.Map.empty all_ids in
-    fun id -> try Id.Map.find id cache with Not_found -> Id.Set.empty in
-  let rec aux s =
-    let s' =
-      Id.Set.fold (fun id s ->
-        if Id.Set.subset (inv_dep_of id) s then Id.Set.diff s (inv_dep_of id)
-        else s)
-      s s in
-    if Id.Set.equal s s' then s else aux s' in
-  aux ids
-
-let suggest_Proof_using kn env vars ids_typ context_ids =
+let remove_ids_and_lets env s ids =
+  let not_ids id = not (Id.Set.mem id ids) in
+  let no_body id = named_body id env = None in
+  let deps id = really_needed env (Id.Set.singleton id) in
+    (Id.Set.filter (fun id ->
+      not_ids id &&
+     (no_body id ||
+       Id.Set.exists not_ids (Id.Set.filter no_body (deps id)))) s)
+
+let suggest_Proof_using name env vars ids_typ context_ids =
   let module S = Id.Set in
   let open Pp in
-  let used = S.union vars ids_typ in
-  let needed = minimize_hyps env used in
-  let all_needed = really_needed env needed in
-  let all = List.fold_right S.add context_ids S.empty in
-  let unneeded = minimize_unused_hyps env (S.diff all needed) in
-  let pr_set s =
+  let print x = prerr_endline (string_of_ppcmds x) in
+  let pr_set parens s =
     let wrap ppcmds =
-      if S.cardinal s > 1 || S.equal s (S.singleton (Id.of_string "All"))
-      then str "(" ++ ppcmds ++ str ")"
+      if parens && S.cardinal s > 1 then str "(" ++ ppcmds ++ str ")"
       else ppcmds in
     wrap (prlist_with_sep (fun _ -> str" ") Id.print (S.elements s)) in
+  let used = S.union vars ids_typ in
+  let needed = minimize_hyps env (remove_ids_and_lets env used ids_typ) in
+  let all_needed = really_needed env needed in
+  let all = List.fold_right S.add context_ids S.empty in
+  let fwd_typ = close_fwd env ids_typ in
   if !Flags.debug then begin
-    prerr_endline (string_of_ppcmds (str "All " ++ pr_set all));
-    prerr_endline (string_of_ppcmds (str "Type" ++ pr_set ids_typ));
-    prerr_endline (string_of_ppcmds (str "needed " ++ pr_set needed));
-    prerr_endline (string_of_ppcmds (str "unneeded " ++ pr_set unneeded));
+    print (str "All "        ++ pr_set false all);
+    print (str "Type "       ++ pr_set false ids_typ);
+    print (str "needed "     ++ pr_set false needed);
+    print (str "all_needed " ++ pr_set false all_needed);
+    print (str "Type* "      ++ pr_set false fwd_typ);
   end;
+  let valid_exprs = ref [] in
+  let valid e = valid_exprs := e :: !valid_exprs in
+  if S.is_empty needed then valid (str "Type");
+  if S.equal all_needed fwd_typ then valid (str "Type*");
+  if S.equal all all_needed then valid(str "All");
+  valid (pr_set false needed);
   msg_info (
-    str"The proof of "++
-    Names.Constant.print kn ++ spc() ++ str "should start with:"++spc()++
-    str"Proof using " ++
-    if S.is_empty needed then str "."
-    else if S.subset needed ids_typ then str "Type."
-    else if S.equal all all_needed then str "All."
-    else 
-      let s1 = string_of_ppcmds (str "-" ++ pr_set unneeded ++ str".") in
-      let s2 = string_of_ppcmds (pr_set needed ++ str".") in
-      if String.length s1 < String.length s2 then str s1 else str s2)
+    str"The proof of "++ str name ++ spc() ++
+    str "should start with one of the following commands:"++spc()++
+    v 0 (
+    prlist_with_sep cut (fun x->str"Proof using " ++x++ str". ") !valid_exprs));
+  string_of_ppcmds (prlist_with_sep (fun _ -> str";")  (fun x->x) !valid_exprs)
+;;
 
 let value = ref false
 
@@ -146,13 +146,13 @@ let _ =
       Goptions.optwrite = (fun b ->
         value := b;
         if b then Term_typing.set_suggest_proof_using suggest_Proof_using
-        else Term_typing.set_suggest_proof_using (fun _ _ _ _ _ -> ())
+        else Term_typing.set_suggest_proof_using (fun _ _ _ _ _ -> "")
       ) }
 
-let value = ref "_unset_"
+let value = ref None
 
 let _ =
-  Goptions.declare_string_option
+  Goptions.declare_stringopt_option
     { Goptions.optsync  = true;
       Goptions.optdepr  = false;
       Goptions.optname  = "default value for Proof using";
@@ -161,6 +161,4 @@ let _ =
       Goptions.optwrite = (fun b -> value := b;) }
 
 
-let get_default_proof_using () =
-  if !value = "_unset_" then None
-  else Some !value
+let get_default_proof_using () = !value
diff --git a/proofs/proof_using.mli b/proofs/proof_using.mli
index fb3497f10..dcf8a0fcd 100644
--- a/proofs/proof_using.mli
+++ b/proofs/proof_using.mli
@@ -6,21 +6,12 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-
-(* [minimize_hyps e s1] gives [s2] s.t. [Id.Set.subset s2 s1] is [true]
- * and [keep_hyps e s1] is equal to [keep_hyps e s2].  Inefficient. *)
-val minimize_hyps : Environ.env -> Names.Id.Set.t -> Names.Id.Set.t
-
-(* [minimize_unused_hyps e s1] gives [s2] s.t. [Id.Set.subset s2 s1] is [true]
- * and s.t. calling [clear s1] would do the same as [clear s2].  Inefficient. *)
-val minimize_unused_hyps : Environ.env -> Names.Id.Set.t -> Names.Id.Set.t
-
 val process_expr :
-  Environ.env -> Vernacexpr.section_subset_descr -> Constr.types list ->
+  Environ.env -> Vernacexpr.section_subset_expr -> Constr.types list ->
     Names.Id.t list
 
-val name_set : Names.Id.t -> Vernacexpr.section_subset_descr -> unit
+val name_set : Names.Id.t -> Vernacexpr.section_subset_expr -> unit
 
-val to_string : Vernacexpr.section_subset_descr -> string
+val to_string : Vernacexpr.section_subset_expr -> string
 
 val get_default_proof_using : unit -> string option
diff --git a/stm/stm.ml b/stm/stm.ml
index d25466e08..acbb5f646 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -888,9 +888,16 @@ let set_compilation_hints file =
   hints := Aux_file.load_aux_file_for file
 let get_hint_ctx loc =
   let s = Aux_file.get !hints loc "context_used" in
-  let ids = List.map Names.Id.of_string (Str.split (Str.regexp " ") s) in
-  let ids = List.map (fun id -> Loc.ghost, id) ids in
-  SsExpr (SsSet ids)
+  match Str.split (Str.regexp ";") s with
+  | ids :: _ ->
+      let ids = List.map Names.Id.of_string (Str.split (Str.regexp " ") ids) in
+      let ids = List.map (fun id -> Loc.ghost, id) ids in
+      begin match ids with
+      | [] -> SsEmpty
+      | x :: xs ->
+          List.fold_left (fun a x -> SsUnion (SsSingl x,a)) (SsSingl x) xs
+      end
+  | _ -> raise Not_found
 
 let get_hint_bp_time proof_name =
   try float_of_string (Aux_file.get !hints Loc.ghost proof_name)
diff --git a/test-suite/success/proof_using.v b/test-suite/success/proof_using.v
index 61e73f858..c83f45e2a 100644
--- a/test-suite/success/proof_using.v
+++ b/test-suite/success/proof_using.v
@@ -117,5 +117,81 @@ End T1.
 
 Check (bla 7 : 2 = 8).
 
+Section A.
+Variable a : nat.
+Variable b : nat.
+Variable c : nat.
+Variable H1 : a = 3.
+Variable H2 : a = 3 -> b = 7.
+Variable H3 : c = 3.
+
+Lemma foo : a = a.
+Proof using Type*.
+pose H1 as e1.
+pose H2 as e2.
+reflexivity.
+Qed.
+
+Lemma bar : a = 3 -> b = 7.
+Proof using b*.
+exact H2.
+Qed.
+
+Lemma baz : c=3.
+Proof using c*.
+exact H3.
+Qed.
+
+Lemma baz2 : c=3.
+Proof using c* a.
+exact H3.
+Qed.
+
+End A.
+
+Check (foo 3 7 (refl_equal 3)
+               (fun _ => refl_equal 7)).
+Check (bar 3 7 (refl_equal 3)
+               (fun _ => refl_equal 7)).
+Check (baz2 99 3 (refl_equal 3)).
+Check (baz 3 (refl_equal 3)).
+
+Section Let.
+
+Variables a b : nat.
+Let pa : a = a. Proof. reflexivity. Qed.
+Unset Default Proof Using.
+Set Suggest Proof Using.
+Lemma test_let : a = a.
+Proof using a.
+exact pa.
+Qed.
+
+Let ppa : pa = pa. Proof. reflexivity. Qed.
+
+Lemma test_let2 : pa = pa.
+Proof using Type.
+exact ppa.
+Qed.
+
+End Let.
+
+Check (test_let 3).
+
+Section Clear.
+
+Variable a: nat.
+Hypotheses H : a = 4.
+
+Set Proof Using Clear Unused.
+
+Lemma test_clear : a = a.
+Proof using a.
+Fail rewrite H.
+trivial.
+Qed.
+
+End Clear.
+
 
 
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 5147d81bc..72c800f0f 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -874,18 +874,7 @@ let vernac_set_used_variables e =
       errorlabstrm "vernac_set_used_variables"
         (str "Unknown variable: " ++ pr_id id))
     l;
-  let closure_l = List.map pi1 (set_used_variables l) 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
+  let _, to_clear = set_used_variables l in
   vernac_solve
     SelectAll None Tacexpr.(TacAtom (Loc.ghost,TacClear(false,to_clear))) false