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.

1 files changed, 5 insertions, 3 deletions

diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml
index 4ece6cb24d..6ea34185fe 100644
--- a/printing/ppvernac.ml
+++ b/printing/ppvernac.ml
@@ -471,6 +471,8 @@ let pr_printable = function
 | PrintNamespace dp -> str "Print Namespace" ++ pr_dirpath dp
 in
 
+let pr_using e = str (Proof_using.to_string e) in
+
 let rec pr_vernac = function
   | VernacProgram v -> str"Program" ++ spc() ++ pr_vernac v
   | VernacLocal (local, v) -> pr_locality local ++ spc() ++ pr_vernac v
@@ -944,10 +946,10 @@ let rec pr_vernac = function
   (* For extension *)
   | VernacExtend (s,c) -> pr_extend s c
   | VernacProof (None, None) -> str "Proof"
-  | VernacProof (None, Some l) -> str "Proof using" ++spc()++ prlist pr_lident l
+  | VernacProof (None, Some e) -> str "Proof " ++ pr_using e
   | VernacProof (Some te, None) -> str "Proof with" ++ spc() ++ pr_raw_tactic te
-  | VernacProof (Some te, Some l) ->
-      str "Proof using" ++spc()++ prlist pr_lident l ++ spc() ++
+  | VernacProof (Some te, Some e) ->
+      str "Proof " ++ pr_using e ++ spc() ++
       str "with" ++ spc() ++pr_raw_tactic te
   | VernacProofMode s -> str ("Proof Mode "^s)
   | VernacBullet b -> begin match b with