Proof using: let-in policy, optional auto-clear, forward closure*

- "Proof using p*" means: use p and any section var about p.
- Simplify the grammar/parser for proof using <expression>.
- Section variables with a body (let-in) are pulled in automatically
  since they are safe to be used (add no extra quantification)
- automatic clear of "unused" section variables made optional:
    Set Proof Using Clear Unused.
  since clearing section hypotheses does not "always work" (e.g. hint
  databases are not really cleaned)
- term_typing: trigger a "suggest proof using" message also for Let
  theorems.

2 files changed, 36 insertions, 22 deletions

diff --git a/parsing/g_proofs.ml4 b/parsing/g_proofs.ml4
index 1e254c16ba..7f5459bfa6 100644
--- a/parsing/g_proofs.ml4
+++ b/parsing/g_proofs.ml4
@@ -37,12 +37,12 @@ GEXTEND Gram
   command:
     [ [ IDENT "Goal"; c = lconstr -> VernacGoal c
       | IDENT "Proof" ->
-          VernacProof (None,hint_proof_using G_vernac.section_subset_descr None)
+          VernacProof (None,hint_proof_using G_vernac.section_subset_expr None)
       | IDENT "Proof" ; IDENT "Mode" ; mn = string -> VernacProofMode mn
       | IDENT "Proof"; "with"; ta = tactic; 
-        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;
+        l = OPT [ "using"; l = G_vernac.section_subset_expr -> l ] ->
+          VernacProof (Some ta,hint_proof_using G_vernac.section_subset_expr l)
+      | IDENT "Proof"; "using"; l = G_vernac.section_subset_expr;
         ta = OPT [ "with"; ta = tactic -> ta ] ->
           VernacProof (ta,Some l)
       | IDENT "Proof"; c = lconstr -> VernacExactProof c
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index e9915fceb3..fc0a4c8c31 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -46,7 +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 section_subset_expr = Gram.entry_create "vernac:section_subset_expr"
 
 let command_entry = ref noedit_mode
 let set_command_entry e = command_entry := e
@@ -447,20 +447,24 @@ GEXTEND Gram
   ;
 END
 
-let only_identrefs =
-  Gram.Entry.of_parser "test_only_identrefs"
+let only_starredidentrefs =
+  Gram.Entry.of_parser "test_only_starredidentrefs"
     (fun strm ->
       let rec aux n =
       match get_tok (Util.stream_nth n strm) with
         | KEYWORD "." -> ()
         | KEYWORD ")" -> ()
-        | IDENT _ -> aux (n+1)
+        | (IDENT _ | KEYWORD "Type" | KEYWORD "*") -> aux (n+1)
         | _ -> raise Stream.Failure in
       aux 0)
+let starredidentreflist_to_expr l =
+  match l with
+  | [] -> SsEmpty
+  | x :: xs -> List.fold_right (fun i acc -> SsUnion(i,acc)) xs x
 
 (* Modules and Sections *)
 GEXTEND Gram
-  GLOBAL: gallina_ext module_expr module_type section_subset_descr;
+  GLOBAL: gallina_ext module_expr module_type section_subset_expr;
 
   gallina_ext:
     [ [ (* Interactive module declaration *)
@@ -483,7 +487,7 @@ GEXTEND Gram
       | IDENT "End"; id = identref -> VernacEndSegment id
 
       (* Naming a set of section hyps *)
-      | IDENT "Collection"; id = identref; ":="; expr = section_subset_descr ->
+      | IDENT "Collection"; id = identref; ":="; expr = section_subset_expr ->
           VernacNameSectionHypSet (id, expr)
 
       (* Requiring an already compiled module *)
@@ -574,22 +578,32 @@ 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 ] ]
-  ;
+  (* Proof using *)
   section_subset_expr:
+    [ [ only_starredidentrefs; l = LIST0 starredidentref ->
+          starredidentreflist_to_expr l
+      | e = ssexpr -> e ]]
+  ;
+  starredidentref:
+    [ [ i = identref -> SsSingl i
+      | i = identref; "*" -> SsFwdClose(SsSingl i)
+      | "Type" -> SsSingl (!@loc, Id.of_string "Type")
+      | "Type"; "*" -> SsFwdClose (SsSingl (!@loc, Id.of_string "Type")) ]]
+  ;
+  ssexpr:
     [ "35" 
-      [ "-"; e = section_subset_expr -> SsCompl e ]
+      [ "-"; e = ssexpr -> 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)]
+      [ e1 = ssexpr; "-"; e2 = ssexpr->SsSubstr(e1,e2)
+      | e1 = ssexpr; "+"; e2 = ssexpr->SsUnion(e1,e2)]
     | "0"
-      [ i = identref -> SsSet [i]
-      | "("; only_identrefs; l = LIST0 identref; ")"-> SsSet l
-      | "("; e = section_subset_expr; ")"-> e ] ]
+      [ i = starredidentref -> i
+      | "("; only_starredidentrefs; l = LIST0 starredidentref; ")"->
+          starredidentreflist_to_expr l
+      | "("; only_starredidentrefs; l = LIST0 starredidentref; ")"; "*" ->
+          SsFwdClose(starredidentreflist_to_expr l)
+      | "("; e = ssexpr; ")"-> e 
+      | "("; e = ssexpr; ")"; "*" -> SsFwdClose e ] ]
   ;
 END