Proof using: New vernacular to name sets of section variables

2 files changed, 37 insertions, 33 deletions

diff --git a/parsing/g_proofs.ml4 b/parsing/g_proofs.ml4
index 2c8eb85b80..60313d749e 100644
--- a/parsing/g_proofs.ml4
+++ b/parsing/g_proofs.ml4
@@ -20,17 +20,6 @@ open Pcoq.Vernac_
 
 let thm_token = G_vernac.thm_token
 
-let only_identrefs =
-  Gram.Entry.of_parser "test_only_identrefs"
-    (fun strm ->
-      let rec aux n =
-      match get_tok (Util.stream_nth n strm) with
-        | KEYWORD "." -> ()
-        | KEYWORD ")" -> ()
-        | IDENT _ -> aux (n+1)
-        | _ -> raise Stream.Failure in
-      aux 0)
-
 let hint_proof_using e = function
   | Some _ as x -> x
   | None -> match Proof_using.get_default_proof_using () with
@@ -48,12 +37,12 @@ GEXTEND Gram
   command:
     [ [ IDENT "Goal"; c = lconstr -> VernacGoal c
       | IDENT "Proof" ->
-          VernacProof (None,hint_proof_using section_subset_descr None)
+          VernacProof (None,hint_proof_using G_vernac.section_subset_descr None)
       | IDENT "Proof" ; IDENT "Mode" ; mn = string -> VernacProofMode mn
       | IDENT "Proof"; "with"; ta = tactic; 
-        l = OPT [ "using"; l = section_subset_descr -> l ] ->
-          VernacProof (Some ta, hint_proof_using section_subset_descr l)
-      | IDENT "Proof"; "using"; l = section_subset_descr;
+        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;
         ta = OPT [ "with"; ta = tactic -> ta ] ->
           VernacProof (ta,Some l)
       | IDENT "Proof"; c = lconstr -> VernacExactProof c
@@ -115,23 +104,6 @@ GEXTEND Gram
 	  VernacHints (false,dbnames,
 	    HintsResolve (List.map (fun x -> (pri, true, x)) lc))
       ] ];
-  section_subset_descr:
-    [ [ IDENT "All" -> SsAll
-      | "Type" -> SsType
-      | only_identrefs; l = LIST0 identref -> SsExpr (SsSet l)
-      | e = section_subset_expr -> SsExpr e ] ]
-  ;
-  section_subset_expr:
-    [ "35" 
-      [ "-"; e = section_subset_expr -> 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)]
-    | "0"
-      [ i = identref -> SsSet [i]
-      | "("; only_identrefs; l = LIST0 identref; ")"-> SsSet l
-      | "("; e = section_subset_expr; ")"-> e ] ]
-  ;
   obsolete_locality:
     [ [ IDENT "Local" -> true | -> false ] ]
   ;
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index ce731a5f54..77ba41f4e0 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -46,6 +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 command_entry = ref noedit_mode
 let set_command_entry e = command_entry := e
@@ -423,10 +424,20 @@ GEXTEND Gram
   ;
 END
 
+let only_identrefs =
+  Gram.Entry.of_parser "test_only_identrefs"
+    (fun strm ->
+      let rec aux n =
+      match get_tok (Util.stream_nth n strm) with
+        | KEYWORD "." -> ()
+        | KEYWORD ")" -> ()
+        | IDENT _ -> aux (n+1)
+        | _ -> raise Stream.Failure in
+      aux 0)
 
 (* Modules and Sections *)
 GEXTEND Gram
-  GLOBAL: gallina_ext module_expr module_type;
+  GLOBAL: gallina_ext module_expr module_type section_subset_descr;
 
   gallina_ext:
     [ [ (* Interactive module declaration *)
@@ -448,6 +459,10 @@ GEXTEND Gram
       (* This end a Section a Module or a Module Type *)
       | IDENT "End"; id = identref -> VernacEndSegment id
 
+      (* Naming a set of section hyps *)
+      | IDENT "Package"; id = identref; ":="; expr = section_subset_descr ->
+          VernacNameSectionHypSet (id, expr)
+
       (* Requiring an already compiled module *)
       | IDENT "Require"; export = export_token; qidl = LIST1 global ->
           VernacRequire (export, qidl)
@@ -537,6 +552,23 @@ 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 ] ]
+  ;
+  section_subset_expr:
+    [ "35" 
+      [ "-"; e = section_subset_expr -> 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)]
+    | "0"
+      [ i = identref -> SsSet [i]
+      | "("; only_identrefs; l = LIST0 identref; ")"-> SsSet l
+      | "("; e = section_subset_expr; ")"-> e ] ]
+  ;
 END
 
 (* Extensions: implicits, coercions, etc. *)