Removing the special status of generic arguments defined by Coq itself.

This makes the TACTIC EXTEND macro insensitive to Coq-defined arguments. They
now have to be reachable in the ML code. Note that this has some consequences,
as the previous macro was potentially mixing grammar entries and arguments as
long as their name was the same. Now, each genarg comes with its grammar
instead, so there is no way to abuse the macro.

6 files changed, 174 insertions, 6 deletions

diff --git a/tactics/coretactics.ml4 b/tactics/coretactics.ml4
index 73b7bde9d7..6c02a7202f 100644
--- a/tactics/coretactics.ml4
+++ b/tactics/coretactics.ml4
@@ -15,6 +15,7 @@ open Misctypes
 open Genredexpr
 open Stdarg
 open Constrarg
+open Extraargs
 open Pcoq.Constr
 open Pcoq.Prim
 open Pcoq.Tactic
diff --git a/tactics/extraargs.ml4 b/tactics/extraargs.ml4
index 8215e785ab..d33ec91f9d 100644
--- a/tactics/extraargs.ml4
+++ b/tactics/extraargs.ml4
@@ -55,6 +55,14 @@ ARGUMENT EXTEND orient TYPED AS bool PRINTED BY pr_orient
 | [ ] -> [ true ]
 END
 
+let pr_int _ _ _ i = Pp.int i
+
+let _natural = Pcoq.Prim.natural
+
+ARGUMENT EXTEND natural TYPED AS int PRINTED BY pr_int
+| [ _natural(i) ] -> [ i ]
+END
+
 let pr_orient = pr_orient () () ()
 
 
@@ -122,6 +130,8 @@ let interp_glob ist gl (t,_) = Tacmach.project gl , (ist,t)
 
 let glob_glob = Tacintern.intern_constr
 
+let pr_lconstr _ prc _ c = prc c
+
 let subst_glob = Tacsubst.subst_glob_constr_and_expr
 
 ARGUMENT EXTEND glob
@@ -139,6 +149,14 @@ ARGUMENT EXTEND glob
   [ constr(c) ] -> [ c ]
 END
 
+let l_constr = Pcoq.Constr.lconstr
+
+ARGUMENT EXTEND lconstr
+    TYPED AS constr
+    PRINTED BY pr_lconstr
+  [ l_constr(c) ] -> [ c ]
+END
+
 ARGUMENT EXTEND lglob
     PRINTED BY pr_globc
 
diff --git a/tactics/extraargs.mli b/tactics/extraargs.mli
index f7b379e69e..14aa69875f 100644
--- a/tactics/extraargs.mli
+++ b/tactics/extraargs.mli
@@ -21,6 +21,8 @@ val wit_occurrences : (int list or_var, int list or_var, int list) Genarg.genarg
 val pr_occurrences : int list or_var -> Pp.std_ppcmds
 val occurrences_of : int list -> Locus.occurrences
 
+val wit_natural : int Genarg.uniform_genarg_type
+
 val wit_glob :
   (constr_expr,
   Tacexpr.glob_constr_and_expr,
@@ -31,6 +33,11 @@ val wit_lglob :
   Tacexpr.glob_constr_and_expr,
   Tacinterp.interp_sign * glob_constr) Genarg.genarg_type
 
+val wit_lconstr :
+  (constr_expr,
+  Tacexpr.glob_constr_and_expr,
+  Constr.t) Genarg.genarg_type
+
 val glob : constr_expr Pcoq.Gram.entry
 val lglob : constr_expr Pcoq.Gram.entry
 
diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4
index 52419497d1..0cc796886c 100644
--- a/tactics/extratactics.ml4
+++ b/tactics/extratactics.ml4
@@ -154,23 +154,23 @@ TACTIC EXTEND einjection
 | [ "einjection" quantified_hypothesis(h) ] -> [ injClause None true (Some (induction_arg_of_quantified_hyp h)) ]
 END
 TACTIC EXTEND injection_as_main
-| [ "injection" constr_with_bindings(c) "as" simple_intropattern_list(ipat)] ->
+| [ "injection" constr_with_bindings(c) "as" intropattern_list(ipat)] ->
     [ elimOnConstrWithHoles (injClause (Some ipat)) false c ]
 END
 TACTIC EXTEND injection_as
-| [ "injection" "as" simple_intropattern_list(ipat)] ->
+| [ "injection" "as" intropattern_list(ipat)] ->
     [ injClause (Some ipat) false None ]
-| [ "injection" quantified_hypothesis(h) "as" simple_intropattern_list(ipat) ] ->
+| [ "injection" quantified_hypothesis(h) "as" intropattern_list(ipat) ] ->
     [ injClause (Some ipat) false (Some (induction_arg_of_quantified_hyp h)) ]
 END
 TACTIC EXTEND einjection_as_main
-| [ "einjection" constr_with_bindings(c) "as" simple_intropattern_list(ipat)] ->
+| [ "einjection" constr_with_bindings(c) "as" intropattern_list(ipat)] ->
     [ elimOnConstrWithHoles (injClause (Some ipat)) true c ]
 END
 TACTIC EXTEND einjection_as
-| [ "einjection" "as" simple_intropattern_list(ipat)] ->
+| [ "einjection" "as" intropattern_list(ipat)] ->
     [ injClause (Some ipat) true None ]
-| [ "einjection" quantified_hypothesis(h) "as" simple_intropattern_list(ipat) ] ->
+| [ "einjection" quantified_hypothesis(h) "as" intropattern_list(ipat) ] ->
     [ injClause (Some ipat) true (Some (induction_arg_of_quantified_hyp h)) ]
 END
 
diff --git a/tactics/g_obligations.ml4 b/tactics/g_obligations.ml4
new file mode 100644
index 0000000000..e67d701218
--- /dev/null
+++ b/tactics/g_obligations.ml4
@@ -0,0 +1,141 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(*i camlp4deps: "grammar/grammar.cma" i*)
+
+(*
+  Syntax for the subtac terms and types.
+  Elaborated from correctness/psyntax.ml4 by Jean-Christophe Filliâtre *)
+
+
+open Libnames
+open Constrexpr
+open Constrexpr_ops
+open Stdarg
+open Constrarg
+open Extraargs
+open Pcoq.Prim
+open Pcoq.Constr
+open Pcoq.Tactic
+
+(* We define new entries for programs, with the use of this module
+ * Subtac. These entries are named Subtac.<foo>
+ *)
+
+module Gram = Pcoq.Gram
+module Vernac = Pcoq.Vernac_
+module Tactic = Pcoq.Tactic
+
+open Pcoq
+
+let sigref = mkRefC (Qualid (Loc.ghost, Libnames.qualid_of_string "Coq.Init.Specif.sig"))
+
+type 'a withtac_argtype = (Tacexpr.raw_tactic_expr option, 'a) Genarg.abstract_argument_type
+
+let wit_withtac : Tacexpr.raw_tactic_expr option Genarg.uniform_genarg_type =
+  Genarg.create_arg "withtac"
+
+let withtac = Pcoq.create_generic_entry Pcoq.utactic "withtac" (Genarg.rawwit wit_withtac)
+
+GEXTEND Gram
+  GLOBAL: withtac;
+
+  withtac:
+    [ [ "with"; t = Tactic.tactic -> Some t
+      | -> None ] ]
+  ;
+
+  Constr.closed_binder:
+    [[ "("; id=Prim.name; ":"; t=Constr.lconstr; "|"; c=Constr.lconstr; ")" ->
+	  let typ = mkAppC (sigref, [mkLambdaC ([id], default_binder_kind, t, c)]) in
+          [LocalRawAssum ([id], default_binder_kind, typ)]
+    ] ];
+
+  END
+
+open Obligations
+
+let classify_obbl _ = Vernacexpr.(VtStartProof ("Classic",Doesn'tGuaranteeOpacity,[]), VtLater)
+
+VERNAC COMMAND EXTEND Obligations CLASSIFIED BY classify_obbl
+| [ "Obligation" integer(num) "of" ident(name) ":" lglob(t) withtac(tac) ] ->
+    [ obligation (num, Some name, Some t) tac ]
+| [ "Obligation" integer(num) "of" ident(name) withtac(tac) ] ->
+    [ obligation (num, Some name, None) tac ]
+| [ "Obligation" integer(num) ":" lglob(t) withtac(tac) ] ->
+    [ obligation (num, None, Some t) tac ]
+| [ "Obligation" integer(num) withtac(tac) ] ->
+    [ obligation (num, None, None) tac ]
+| [ "Next" "Obligation" "of" ident(name) withtac(tac) ] ->
+    [ next_obligation (Some name) tac ]
+| [ "Next" "Obligation" withtac(tac) ] -> [ next_obligation None tac ]
+END
+
+VERNAC COMMAND EXTEND Solve_Obligation CLASSIFIED AS SIDEFF
+| [ "Solve" "Obligation" integer(num) "of" ident(name) "with" tactic(t) ] ->
+    [ try_solve_obligation num (Some name) (Some (Tacinterp.interp t)) ]
+| [ "Solve" "Obligation" integer(num) "with" tactic(t) ] ->
+    [ try_solve_obligation num None (Some (Tacinterp.interp t)) ]
+END
+
+VERNAC COMMAND EXTEND Solve_Obligations CLASSIFIED AS SIDEFF
+| [ "Solve" "Obligations" "of" ident(name) "with" tactic(t) ] ->
+    [ try_solve_obligations (Some name) (Some (Tacinterp.interp t)) ]
+| [ "Solve" "Obligations" "with" tactic(t) ] ->
+    [ try_solve_obligations None (Some (Tacinterp.interp t)) ]
+| [ "Solve" "Obligations" ] ->
+    [ try_solve_obligations None None ]
+END
+
+VERNAC COMMAND EXTEND Solve_All_Obligations CLASSIFIED AS SIDEFF
+| [ "Solve" "All" "Obligations" "with" tactic(t) ] ->
+    [ solve_all_obligations (Some (Tacinterp.interp t)) ]
+| [ "Solve" "All" "Obligations" ] ->
+    [ solve_all_obligations None ]
+END
+
+VERNAC COMMAND EXTEND Admit_Obligations CLASSIFIED AS SIDEFF
+| [ "Admit" "Obligations" "of" ident(name) ] -> [ admit_obligations (Some name) ]
+| [ "Admit" "Obligations" ] -> [ admit_obligations None ]
+END
+
+VERNAC COMMAND EXTEND Set_Solver CLASSIFIED AS SIDEFF
+| [ "Obligation" "Tactic" ":=" tactic(t) ] -> [
+    set_default_tactic
+      (Locality.make_section_locality (Locality.LocalityFixme.consume ()))
+      (Tacintern.glob_tactic t) ]
+END
+
+open Pp
+
+VERNAC COMMAND EXTEND Show_Solver CLASSIFIED AS QUERY
+| [ "Show" "Obligation" "Tactic" ] -> [
+    msg_info (str"Program obligation tactic is " ++ print_default_tactic ()) ]
+END
+
+VERNAC COMMAND EXTEND Show_Obligations CLASSIFIED AS QUERY
+| [ "Obligations" "of" ident(name) ] -> [ show_obligations (Some name) ]
+| [ "Obligations" ] -> [ show_obligations None ]
+END
+
+VERNAC COMMAND EXTEND Show_Preterm CLASSIFIED AS QUERY
+| [ "Preterm" "of" ident(name) ] -> [ msg_info (show_term (Some name)) ]
+| [ "Preterm" ] -> [ msg_info (show_term None) ]
+END
+
+open Pp
+
+(* Declare a printer for the content of Program tactics *)
+let () =
+  let printer _ _ _ = function
+  | None -> mt ()
+  | Some tac -> str "with" ++ spc () ++ Pptactic.pr_raw_tactic tac
+  in
+  (* should not happen *)
+  let dummy _ _ _ expr = assert false in
+  Pptactic.declare_extra_genarg_pprule wit_withtac printer dummy dummy
diff --git a/tactics/hightactics.mllib b/tactics/hightactics.mllib
index 73f11d0be0..5c59465429 100644
--- a/tactics/hightactics.mllib
+++ b/tactics/hightactics.mllib
@@ -1,4 +1,5 @@
 Extraargs
+G_obligations
 Coretactics
 Autorewrite
 Extratactics