Proof_using: new syntax + suggestion

Proof using can be followed by:
- All : all variables
- Type : all variables occurring in the type
- expr:
    - (a b .. c) : set
    - expr + expr : set union
    - expr - expr : set difference
    - -expr : set complement (All - expr)
Exceptions:
- a singleton set can be written without parentheses. This also allows
  the implementation of named sets sharing the same name space of
  section hyps ans write
  - bla - x : where bla is defined as (a b .. x y) elsewhere.
- if expr is just a set, then parentheses can be omitted

This module also implements some AI to tell the user how he could
decorate "Proof" with a "using BLA" clause.

Finally, one can Set Default Proof Using "str" to any string that is
used whenever the "using ..." part is missing.  The coding of this
sucks a little since it is the parser that applies the default.

3 files changed, 8 insertions, 5 deletions

diff --git a/toplevel/stm.ml b/toplevel/stm.ml
index 57bbafac3a..c0ad017583 100644
--- a/toplevel/stm.ml
+++ b/toplevel/stm.ml
@@ -581,7 +581,7 @@ 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
-  ids
+  SsExpr (SsSet ids)
 
 (* Slave processes (if initialized, otherwise local lazy evaluation) *)
 module Slaves : sig
diff --git a/toplevel/vernac_classifier.ml b/toplevel/vernac_classifier.ml
index 37ab694b6d..3c14d5922f 100644
--- a/toplevel/vernac_classifier.ml
+++ b/toplevel/vernac_classifier.ml
@@ -92,6 +92,9 @@ let rec classify_vernac e =
     | VernacCheckGuard
     | VernacUnfocused
     | VernacSolveExistential _ -> VtProofStep, VtLater
+    (* Options changing parser *)
+    | VernacUnsetOption (["Default";"Proof";"Using"])
+    | VernacSetOption (["Default";"Proof";"Using"],_) -> VtSideff [], VtNow
     (* StartProof *)
     | VernacDefinition (_,(_,i),ProveBody _) ->
         VtStartProof("Classic",GuaranteesOpacity,[i]), VtLater
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index b8a368c823..90d2029eaf 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -798,10 +798,10 @@ let vernac_set_end_tac tac =
   | _ -> set_end_tac tac
     (* TO DO verifier s'il faut pas mettre exist s | TacId s ici*)
 
-let vernac_set_used_variables l =
-  let l = List.map snd l in
-  if not (List.distinct_f Id.compare l)
-  then error "Used variables list contains duplicates";
+let vernac_set_used_variables e =
+  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
   List.iter (fun id -> 
     if not (List.exists (fun (id',_,_) -> Id.equal id id') vars) then