[vernac] Remove "Proof using" hacks from parser.

We place `Proof_using` in the proper place [`vernac`] and we remove
gross parsing hacks.

The new placement should allow to use the printers and more convenient
structure, and reduce strange coupling between parsing and internal
representation.

10 files changed, 37 insertions, 24 deletions

diff --git a/API/API.mli b/API/API.mli
index 04c69b025f..879323a37d 100644
--- a/API/API.mli
+++ b/API/API.mli
@@ -4914,7 +4914,6 @@ module G_proofs :
 sig
 
   val hint : Vernacexpr.hints_expr Pcoq.Gram.entry
-  val hint_proof_using : 'a Pcoq.Gram.entry -> 'a option -> 'a option
 
 end
 
diff --git a/parsing/g_proofs.ml4 b/parsing/g_proofs.ml4
index e2c87bbbf6..f10d746770 100644
--- a/parsing/g_proofs.ml4
+++ b/parsing/g_proofs.ml4
@@ -17,12 +17,6 @@ open Pcoq.Vernac_
 
 let thm_token = G_vernac.thm_token
 
-let hint_proof_using e = function
-  | Some _ as x -> x
-  | None -> match Proof_using.get_default_proof_using () with
-     | None -> None
-     | Some s -> Some (Gram.entry_parse e (Gram.parsable (Stream.of_string s)))
-
 let hint = Gram.entry_create "hint"
 
 (* Proof commands *)
@@ -35,8 +29,7 @@ GEXTEND Gram
   ;
   command:
     [ [ IDENT "Goal"; c = lconstr -> VernacGoal c
-      | IDENT "Proof" ->
-          VernacProof (None,hint_proof_using G_vernac.section_subset_expr None)
+      | IDENT "Proof" -> VernacProof (None,None)
       | IDENT "Proof" ; IDENT "Mode" ; mn = string -> VernacProofMode mn
       | IDENT "Proof"; c = lconstr -> VernacExactProof c
       | IDENT "Abort" -> VernacAbort None
diff --git a/plugins/ltac/g_ltac.ml4 b/plugins/ltac/g_ltac.ml4
index d639dd0e1c..c577cb2198 100644
--- a/plugins/ltac/g_ltac.ml4
+++ b/plugins/ltac/g_ltac.ml4
@@ -340,7 +340,7 @@ GEXTEND Gram
   command:
     [ [ IDENT "Proof"; "with"; ta = Pltac.tactic; 
         l = OPT [ "using"; l = G_vernac.section_subset_expr -> l ] ->
-          Vernacexpr.VernacProof (Some (in_tac ta), G_proofs.hint_proof_using G_vernac.section_subset_expr l)
+          Vernacexpr.VernacProof (Some (in_tac ta), l)
       | IDENT "Proof"; "using"; l = G_vernac.section_subset_expr;
         ta = OPT [ "with"; ta = Pltac.tactic -> in_tac ta ] ->
           Vernacexpr.VernacProof (ta,Some l) ] ]
diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml
index a1cdfdbaa2..4c68285f3f 100644
--- a/printing/ppvernac.ml
+++ b/printing/ppvernac.ml
@@ -524,7 +524,15 @@ open Decl_kinds
     | PrintStrategy (Some qid) ->
       keyword "Print Strategy" ++ pr_smart_global qid
 
-  let pr_using e = str (Proof_using.to_string e)
+  let pr_using 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 Pp.str (aux e)
 
   let rec pr_vernac_body v =
     let return = tag_vernac v in
diff --git a/printing/ppvernac.mli b/printing/ppvernac.mli
index b88eed4843..cf27b413c0 100644
--- a/printing/ppvernac.mli
+++ b/printing/ppvernac.mli
@@ -15,5 +15,8 @@ val pr_rec_definition : (Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation lis
 (** Prints a vernac expression *)
 val pr_vernac_body : Vernacexpr.vernac_expr -> Pp.t
 
+(** Prints a "proof using X" clause. *)
+val pr_using : Vernacexpr.section_subset_expr -> Pp.t
+
 (** Prints a vernac expression and closes it with a dot. *)
 val pr_vernac : Vernacexpr.vernac_expr -> Pp.t
diff --git a/proofs/proofs.mllib b/proofs/proofs.mllib
index eaf0c693e1..058e839b47 100644
--- a/proofs/proofs.mllib
+++ b/proofs/proofs.mllib
@@ -1,7 +1,6 @@
 Miscprint
 Goal
 Evar_refiner
-Proof_using
 Proof_type
 Logic
 Refine
diff --git a/proofs/proof_using.ml b/vernac/proof_using.ml
index 9bfc8bada8..5cc348095e 100644
--- a/proofs/proof_using.ml
+++ b/vernac/proof_using.ml
@@ -185,13 +185,16 @@ let suggest_variable env id =
 
 let value = ref None
 
+let using_to_string us = Pp.string_of_ppcmds (Ppvernac.pr_using us)
+let using_from_string us = Pcoq.Gram.(entry_parse G_vernac.section_subset_expr (parsable (Stream.of_string us)))
+
 let _ =
   Goptions.declare_stringopt_option
     { Goptions.optdepr  = false;
       Goptions.optname  = "default value for Proof using";
       Goptions.optkey   = ["Default";"Proof";"Using"];
-      Goptions.optread  = (fun () -> !value);
-      Goptions.optwrite = (fun b -> value := b;) }
-
+      Goptions.optread  = (fun () -> Option.map using_to_string !value);
+      Goptions.optwrite = (fun b -> value := Option.map using_from_string b);
+    }
 
 let get_default_proof_using () = !value
diff --git a/proofs/proof_using.mli b/vernac/proof_using.mli
index ac2795f806..ddab2742d7 100644
--- a/proofs/proof_using.mli
+++ b/vernac/proof_using.mli
@@ -20,4 +20,4 @@ val suggest_constant : Environ.env -> Names.Constant.t -> unit
 
 val suggest_variable : Environ.env -> Names.Id.t -> unit
 
-val get_default_proof_using : unit -> string option
+val get_default_proof_using : unit -> Vernacexpr.section_subset_expr option
diff --git a/vernac/vernac.mllib b/vernac/vernac.mllib
index f74073e1f7..850902d6ba 100644
--- a/vernac/vernac.mllib
+++ b/vernac/vernac.mllib
@@ -1,4 +1,5 @@
 Vernacprop
+Proof_using
 Lemmas
 Himsg
 ExplainErr
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 203d913db8..4af4b642ca 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -2060,17 +2060,24 @@ let interp ?proof ?loc locality poly c =
   | VernacEndSubproof -> vernac_end_subproof ()
   | VernacShow s -> vernac_show s
   | VernacCheckGuard -> vernac_check_guard ()
-  | VernacProof (None, None) ->
+  | VernacProof (None, using) ->
+    begin match Option.append using (Proof_using.get_default_proof_using ()) with
+    | None   ->
       Aux_file.record_in_aux_at ?loc "VernacProof" "tac:no using:no"
-  | VernacProof (Some tac, None) ->
-      Aux_file.record_in_aux_at ?loc "VernacProof" "tac:yes using:no";
-      vernac_set_end_tac tac
-  | VernacProof (None, Some l) ->
+    | Some l ->
       Aux_file.record_in_aux_at ?loc "VernacProof" "tac:no using:yes";
       vernac_set_used_variables l
-  | VernacProof (Some tac, Some l) -> 
-      Aux_file.record_in_aux_at ?loc "VernacProof" "tac:yes using:yes";
-      vernac_set_end_tac tac; vernac_set_used_variables l
+    end
+  | VernacProof (Some tac, using) ->
+    begin match Option.append using (Proof_using.get_default_proof_using ()) with
+      | None ->
+        Aux_file.record_in_aux_at ?loc "VernacProof" "tac:yes using:no";
+        vernac_set_end_tac tac
+      | Some l ->
+        Aux_file.record_in_aux_at ?loc "VernacProof" "tac:yes using:yes";
+        vernac_set_end_tac tac;
+        vernac_set_used_variables l
+    end
   | VernacProofMode mn -> Proof_global.set_proof_mode mn [@ocaml.warning "-3"]
 
   (* Extensions *)