Rationalizing the use of the various EXTEND macros.

Those macros used to handle in a special way the grammar entries and generic
arguments known statically from Coq, i.e. defined before Pcoq. This was hardly
predictible and very implementation-dependent.

We made the EXTEND macros much more light-weight by treating in a uniform way
all entries and arguments. Now, they are all produced by outputing the name
as-is for entries and as "wit_$name" for genargs, thus letting the scope
of the ML code decide which entrie is going to be taken. This is documented
in the dev/ changelog.

This also allows to get rid of a lot of dependencies in the grammar preprocessor,
reducing it to a small functional shell. It is still depending on Compat, but it
is most probably possible to reduce the code size even more.

9 files changed, 208 insertions, 10 deletions

diff --git a/tactics/coretactics.ml4 b/tactics/coretactics.ml4
index 7da6df717e..6c02a7202f 100644
--- a/tactics/coretactics.ml4
+++ b/tactics/coretactics.ml4
@@ -13,6 +13,12 @@ open Names
 open Locus
 open Misctypes
 open Genredexpr
+open Stdarg
+open Constrarg
+open Extraargs
+open Pcoq.Constr
+open Pcoq.Prim
+open Pcoq.Tactic
 
 open Proofview.Notations
 open Sigma.Notations
@@ -143,7 +149,7 @@ END
 
 TACTIC EXTEND symmetry
   [ "symmetry" ] -> [ Tactics.intros_symmetry {onhyps=Some[];concl_occs=AllOccurrences} ]
-| [ "symmetry" clause(cl) ] -> [ Tactics.intros_symmetry cl ]
+| [ "symmetry" clause_dft_concl(cl) ] -> [ Tactics.intros_symmetry cl ]
 END
 
 (** Split *)
diff --git a/tactics/extraargs.ml4 b/tactics/extraargs.ml4
index 98868e8f91..d33ec91f9d 100644
--- a/tactics/extraargs.ml4
+++ b/tactics/extraargs.ml4
@@ -10,6 +10,10 @@
 
 open Pp
 open Genarg
+open Stdarg
+open Constrarg
+open Pcoq.Prim
+open Pcoq.Constr
 open Names
 open Tacexpr
 open Taccoerce
@@ -51,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 () () ()
 
 
@@ -118,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
@@ -135,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 7df845e4bd..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
 
@@ -53,7 +60,6 @@ val pr_by_arg_tac :
   (int * Ppextend.parenRelation -> raw_tactic_expr -> Pp.std_ppcmds) ->
   raw_tactic_expr option -> Pp.std_ppcmds
 
-
 (** Spiwack: Primitive for retroknowledge registration *)
 
 val retroknowledge_field : Retroknowledge.field Pcoq.Gram.entry
diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4
index ae8b83b95e..0cc796886c 100644
--- a/tactics/extratactics.ml4
+++ b/tactics/extratactics.ml4
@@ -10,7 +10,12 @@
 
 open Pp
 open Genarg
+open Stdarg
+open Constrarg
 open Extraargs
+open Pcoq.Prim
+open Pcoq.Constr
+open Pcoq.Tactic
 open Mod_subst
 open Names
 open Tacexpr
@@ -49,6 +54,8 @@ let replace_in_clause_maybe_by ist c1 c2 cl tac =
 let replace_term ist dir_opt c cl =
   with_delayed_uconstr ist c (fun c -> replace_term dir_opt c cl)
 
+let clause = Pcoq.Tactic.clause_dft_concl
+
 TACTIC EXTEND replace
    ["replace" uconstr(c1) "with" constr(c2) clause(cl) by_arg_tac(tac) ]
 -> [ replace_in_clause_maybe_by ist c1 c2 cl tac ]
@@ -147,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_auto.ml4 b/tactics/g_auto.ml4
index f4fae763fd..788443944f 100644
--- a/tactics/g_auto.ml4
+++ b/tactics/g_auto.ml4
@@ -10,6 +10,11 @@
 
 open Pp
 open Genarg
+open Stdarg
+open Constrarg
+open Pcoq.Prim
+open Pcoq.Constr
+open Pcoq.Tactic
 open Tacexpr
 
 DECLARE PLUGIN "g_auto"
@@ -128,7 +133,7 @@ TACTIC EXTEND dfs_eauto
 END
 
 TACTIC EXTEND autounfold
-| [ "autounfold" hintbases(db) clause(cl) ] -> [ Eauto.autounfold_tac db cl ]
+| [ "autounfold" hintbases(db) clause_dft_concl(cl) ] -> [ Eauto.autounfold_tac db cl ]
 END
 
 TACTIC EXTEND autounfold_one
diff --git a/tactics/g_class.ml4 b/tactics/g_class.ml4
index 766593543c..9ef1545416 100644
--- a/tactics/g_class.ml4
+++ b/tactics/g_class.ml4
@@ -10,6 +10,11 @@
 
 open Misctypes
 open Class_tactics
+open Pcoq.Prim
+open Pcoq.Constr
+open Pcoq.Tactic
+open Stdarg
+open Constrarg
 
 DECLARE PLUGIN "g_class"
 
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/g_rewrite.ml4 b/tactics/g_rewrite.ml4
index 8b012aa88e..c4ef1f297e 100644
--- a/tactics/g_rewrite.ml4
+++ b/tactics/g_rewrite.ml4
@@ -20,6 +20,11 @@ open Extraargs
 open Tacmach
 open Tacticals
 open Rewrite
+open Stdarg
+open Constrarg
+open Pcoq.Prim
+open Pcoq.Constr
+open Pcoq.Tactic
 
 DECLARE PLUGIN "g_rewrite"
 
@@ -186,7 +191,7 @@ type binders_argtype = local_binder list
 let wit_binders =
  (Genarg.create_arg "binders" : binders_argtype Genarg.uniform_genarg_type)
 
-let binders = Pcoq.create_generic_entry "binders" (Genarg.rawwit wit_binders)
+let binders = Pcoq.create_generic_entry Pcoq.utactic "binders" (Genarg.rawwit wit_binders)
 
 open Pcoq
 
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