Better doc and a few fixes for Proof using.

6 files changed, 68 insertions, 21 deletions

diff --git a/CHANGES b/CHANGES
index 5f23119d9..56a325937 100644
--- a/CHANGES
+++ b/CHANGES
@@ -70,6 +70,9 @@ Vernacular commands
 - "Undo" undoes any command, not just tactics.
 - New "Refine Instance Mode" option that allows to deactivate the generation of
   obligations in incomplete typeclass instances, raising an error instead.
+- "Collection" command to name sets of section hypotheses.  Named collections
+  can be used in the syntax of "Proof using" to assert with section variables
+  are used in a proof.
 
 Specification Language
 
@@ -280,7 +283,7 @@ Tools
 
 Interfaces
 
-- CoqIDE uses the new STM machinery, allowing for asynchronous edition.
+- CoqIDE supports asynchronous edition of the document.
 - CoqIDE highlight in yellow "unsafe" commands such as axiom
   declarations, and tactics like "admit".
 - Coqtop outputs highlighted syntax. Colors can be configured thanks
diff --git a/doc/refman/RefMan-pro.tex b/doc/refman/RefMan-pro.tex
index 789297fb4..4084424e8 100644
--- a/doc/refman/RefMan-pro.tex
+++ b/doc/refman/RefMan-pro.tex
@@ -153,6 +153,7 @@ in Section~\ref{ProofWith}.
   Use all section variables.
 
 \variant {\tt Proof using Type.} 
+\variant {\tt Proof using.} 
   
   Use only section variables occurring in the statement.
 
@@ -160,6 +161,14 @@ in Section~\ref{ProofWith}.
   
   Use all section variables except {\ident$_1$} {\ldots} {\ident$_n$}.
 
+\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 ).}
+
+  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
+  collection.
+
 \subsubsection{{\tt Proof using} options}
 \comindex{Default Proof Using}
 \comindex{Suggest Proof Using}
@@ -177,24 +186,30 @@ 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.
 
-\subsubsection[\tt Package]{Name a set of section hypotheses for {\tt Proof using}}
-\comindex{Package}
+\subsubsection[\tt Collection]{Name a set of section hypotheses for {\tt Proof using}}
+\comindex{Collection}\label{Collection}
 
-The command {\tt Package} can be used to name a set of section hypotheses,
+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.
 
-\variant {\tt Package Some := x y z.}
+\variant {\tt Collection Some := x y z.}
 
-  Define the package named "Some" containing {\tt x y} and {\tt z} 
+  Define the collection named "Some" containing {\tt x y} and {\tt z} 
 
-\variant {\tt Package Fewer := Some - x.} 
+\variant {\tt Collection Fewer := Some - x.} 
   
-  Define the package named "Fewer" containing only {\tt x y} 
+  Define the collection named "Fewer" containing only {\tt x y} 
 
-\variant {\tt Package Many := Fewer + Some.} 
+\variant {\tt Collection Many := Fewer + Some.} 
+\variant {\tt Collection Many := Fewer - Some.} 
   
-  Define the package named "Many" containing the union of the elements
-  of "Fewer" and "Some", namely {\tt x y z}. 
+  Define the collection named "Many" containing the set union or set difference
+  of "Fewer" and "Some".
+
+\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}.
 
 \subsection[\tt Abort.]{\tt Abort.\comindex{Abort}}
 
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index 77ba41f4e..ccfe3cc8c 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -460,7 +460,7 @@ GEXTEND Gram
       | IDENT "End"; id = identref -> VernacEndSegment id
 
       (* Naming a set of section hyps *)
-      | IDENT "Package"; id = identref; ":="; expr = section_subset_descr ->
+      | IDENT "Collection"; id = identref; ":="; expr = section_subset_descr ->
           VernacNameSectionHypSet (id, expr)
 
       (* Requiring an already compiled module *)
diff --git a/proofs/proof_using.ml b/proofs/proof_using.ml
index f326548d1..144646f3e 100644
--- a/proofs/proof_using.ml
+++ b/proofs/proof_using.ml
@@ -14,7 +14,7 @@ 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(SsSet l)-> String.concat " " (List.map Id.to_string (List.map snd l))
   | SsExpr e ->
       let rec aux = function
         | SsSet [] -> "( )"
@@ -49,16 +49,22 @@ let rec process_expr env e ty =
       in
         aux e
   | SsType ->
-      match ty with
-      | [ty] -> global_vars_set env ty
-      | _ -> Errors.error"Proof using on a multiple lemma is not supported"
+      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))
 
-let process_expr env e ty = Id.Set.elements (process_expr env e ty)
+let process_expr env e ty =
+  let s = Id.Set.union (process_expr env SsType ty) (process_expr env e []) in
+  let l = Id.Set.elements s in
+  Pp.msg_warning Pp.(str(to_string e) ++ spc() ++ str "-> "++
+(*     prlist_with_sep spc Ppconstr.pr_constr ty ++ spc() ++ *)
+    prlist_with_sep spc Nameops.pr_id l);
+  l
 
 let name_set id expr = Lib.add_anonymous_leaf (in_nameset (id,expr))
 
diff --git a/test-suite/success/proof_using.v b/test-suite/success/proof_using.v
index d2691e763..dbbd57ae0 100644
--- a/test-suite/success/proof_using.v
+++ b/test-suite/success/proof_using.v
@@ -73,15 +73,15 @@ Variable y : nat.
 Variable z : nat.
 
 
-Package TOTO := x y.
+Collection TOTO := x y.
 
-Package TITI := TOTO - x.
+Collection TITI := TOTO - x.
 
 Lemma t1 : True. Proof using TOTO. trivial. Qed.
 Lemma t2 : True. Proof using TITI. trivial. Qed.
 
  Section P2.
- Package TOTO := x.
+ Collection TOTO := x.
  Lemma t3 : True. Proof using TOTO. trivial. Qed.
  End P2.
 
@@ -96,3 +96,25 @@ Check (t2 1 : True).
 Check (t3 1 : True).
 Check (t4 1 2 : True).
 
+
+Section T1.
+
+Variable x : nat.
+Hypothesis px : 1 = x.
+Let w := x + 1.
+
+Set Suggest Proof Using.
+
+Set Default Proof Using "Type".
+
+Lemma bla : 2 = w.
+Proof.
+admit.
+Qed.
+
+End T1.
+
+Check (bla 7 : 2 = 8).
+
+
+
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 29ba18307..cd1dad694 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -848,7 +848,8 @@ let vernac_set_end_tac tac =
 
 let vernac_set_used_variables e =
   let tys =
-    List.map fst (Proof.initial_goals (Proof_global.give_me_the_proof ())) in
+    List.map snd (Proof.initial_goals (Proof_global.give_me_the_proof ())) in
+  Pp.(msg_warning (prlist_with_sep spc Printer.pr_constr tys));
   let l = Proof_using.process_expr (Global.env ()) e tys in
   let vars = Environ.named_context (Global.env ()) in
   List.iter (fun id ->