Port remaining EXTEND ml4 files to coqpp.

Almost all of ml4 were removed in the process. The only remaining files
are in the test-suite and probably need a bit of fiddling with coq_makefile,
and there only two really remaning ml4 files containing code.

1 files changed, 77 insertions, 42 deletions

diff --git a/plugins/funind/g_indfun.ml4 b/plugins/funind/g_indfun.mlg
index c7555c44eb..857215751a 100644
--- a/plugins/funind/g_indfun.ml4
+++ b/plugins/funind/g_indfun.mlg
@@ -7,6 +7,9 @@
 (*         *     GNU Lesser General Public License Version 2.1          *)
 (*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
+
+{
+
 open Ltac_plugin
 open Util
 open Pp
@@ -16,13 +19,16 @@ open Indfun
 open Stdarg
 open Tacarg
 open Tactypes
-open Pcoq
 open Pcoq.Prim
 open Pcoq.Constr
 open Pltac
 
+}
+
 DECLARE PLUGIN "recdef_plugin"
 
+{
+
 let pr_fun_ind_using  prc prlc _ opt_c =
   match opt_c with
     | None -> mt ()
@@ -43,24 +49,27 @@ let pr_fun_ind_using_typed prc prlc _ opt_c =
       let (_, b) = b env evd in
       spc () ++ hov 2 (str "using" ++ spc () ++ Miscprint.pr_with_bindings prc prlc b)
 
+}
 
 ARGUMENT EXTEND fun_ind_using
   TYPED AS constr_with_bindings option
-  PRINTED BY pr_fun_ind_using_typed
-  RAW_PRINTED BY pr_fun_ind_using
-  GLOB_PRINTED BY pr_fun_ind_using
-| [ "using" constr_with_bindings(c) ] -> [ Some c ]
-| [ ] -> [ None ]
+  PRINTED BY { pr_fun_ind_using_typed }
+  RAW_PRINTED BY { pr_fun_ind_using }
+  GLOB_PRINTED BY { pr_fun_ind_using }
+| [ "using" constr_with_bindings(c) ] -> { Some c }
+| [ ] -> { None }
 END
 
 
 TACTIC EXTEND newfuninv
-   [ "functional" "inversion"  quantified_hypothesis(hyp) reference_opt(fname) ] ->
-     [
+| [ "functional" "inversion"  quantified_hypothesis(hyp) reference_opt(fname) ] ->
+     {
        Proofview.V82.tactic (Invfun.invfun hyp fname)
-     ]
+     }
 END
 
+{
+
 let pr_intro_as_pat _prc _ _ pat =
   match pat with
     | Some pat ->
@@ -72,56 +81,70 @@ let out_disjunctive = CAst.map (function
   | IntroAction (IntroOrAndPattern l) -> l
   | _ -> CErrors.user_err Pp.(str "Disjunctive or conjunctive intro pattern expected."))
 
-ARGUMENT EXTEND with_names TYPED AS intropattern_opt PRINTED BY pr_intro_as_pat
-|   [ "as"  simple_intropattern(ipat) ] -> [ Some ipat ]
-| []  ->[ None ]
+}
+
+ARGUMENT EXTEND with_names TYPED AS intropattern option PRINTED BY { pr_intro_as_pat }
+| [ "as"  simple_intropattern(ipat) ] -> { Some ipat }
+| []  -> { None }
 END
 
+{
+
 let functional_induction b c x pat =
   Proofview.V82.tactic (functional_induction true c x (Option.map out_disjunctive pat))
 
+}
 
 TACTIC EXTEND newfunind
-   ["functional" "induction" ne_constr_list(cl) fun_ind_using(princl) with_names(pat)] ->
-     [
+| ["functional" "induction" ne_constr_list(cl) fun_ind_using(princl) with_names(pat)] ->
+     {
        let c = match cl with
 	 | [] -> assert false
 	 | [c] -> c
 	 | c::cl -> EConstr.applist(c,cl)
        in
-       Extratactics.onSomeWithHoles (fun x -> functional_induction true c x pat) princl ]
+       Extratactics.onSomeWithHoles (fun x -> functional_induction true c x pat) princl }
 END
 (***** debug only ***)
 TACTIC EXTEND snewfunind
-   ["soft" "functional" "induction" ne_constr_list(cl) fun_ind_using(princl) with_names(pat)] ->
-     [
+| ["soft" "functional" "induction" ne_constr_list(cl) fun_ind_using(princl) with_names(pat)] ->
+     {
        let c = match cl with
 	 | [] -> assert false
 	 | [c] -> c
 	 | c::cl -> EConstr.applist(c,cl)
        in
-       Extratactics.onSomeWithHoles (fun x -> functional_induction false c x pat) princl ]
+       Extratactics.onSomeWithHoles (fun x -> functional_induction false c x pat) princl }
 END
 
+{
 
 let pr_constr_comma_sequence prc _ _ = prlist_with_sep pr_comma prc
 
+}
+
 ARGUMENT EXTEND constr_comma_sequence'
-  TYPED AS constr_list
-  PRINTED BY pr_constr_comma_sequence
-| [ constr(c) "," constr_comma_sequence'(l) ] -> [ c::l ]
-| [ constr(c) ] -> [ [c] ]
+  TYPED AS constr list
+  PRINTED BY { pr_constr_comma_sequence }
+| [ constr(c) "," constr_comma_sequence'(l) ] -> { c::l }
+| [ constr(c) ] -> { [c] }
 END
 
+{
+
 let pr_auto_using prc _prlc _prt = Pptactic.pr_auto_using prc
 
+}
+
 ARGUMENT EXTEND auto_using'
-  TYPED AS constr_list
-  PRINTED BY pr_auto_using
-| [ "using" constr_comma_sequence'(l) ] -> [ l ]
-| [ ] -> [ [] ]
+  TYPED AS constr list
+  PRINTED BY { pr_auto_using }
+| [ "using" constr_comma_sequence'(l) ] -> { l }
+| [ ] -> { [] }
 END
 
+{
+
 module Gram = Pcoq.Gram
 module Vernac = Pvernac.Vernac_
 module Tactic = Pltac
@@ -134,23 +157,29 @@ let (wit_function_rec_definition_loc : function_rec_definition_loc_argtype Genar
 let function_rec_definition_loc =
   Pcoq.create_generic_entry Pcoq.utactic "function_rec_definition_loc" (Genarg.rawwit wit_function_rec_definition_loc)
 
-GEXTEND Gram
+}
+
+GRAMMAR EXTEND Gram
   GLOBAL: function_rec_definition_loc ;
 
   function_rec_definition_loc:
-    [ [ g = Vernac.rec_definition -> Loc.tag ~loc:!@loc g ]]
+    [ [ g = Vernac.rec_definition -> { Loc.tag ~loc g } ]]
     ;
 
 END
 
+{
+
 let () =
   let raw_printer _ _ _ (loc,body) = Ppvernac.pr_rec_definition body in
   Pptactic.declare_extra_vernac_genarg_pprule wit_function_rec_definition_loc raw_printer
 
+}
+
 (* TASSI: n'importe quoi ! *)
 VERNAC COMMAND EXTEND Function
-   ["Function" ne_function_rec_definition_loc_list_sep(recsl,"with")]
-    => [ let hard = List.exists (function
+| ["Function" ne_function_rec_definition_loc_list_sep(recsl,"with")]
+    => { let hard = List.exists (function
            | _,((_,(_,(CMeasureRec _|CWfRec _)),_,_,_),_) -> true
            | _,((_,(_,CStructRec),_,_,_),_) -> false) recsl in
          match
@@ -159,20 +188,25 @@ VERNAC COMMAND EXTEND Function
          with
          | Vernacexpr.VtSideff ids, _ when hard ->
              Vernacexpr.(VtStartProof ("Classic", GuaranteesOpacity, ids), VtLater)
-         | x -> x ]
-    -> [ do_generate_principle false (List.map snd recsl) ]
+         | x -> x }
+    -> { do_generate_principle false (List.map snd recsl) }
 END
 
+{
+
 let pr_fun_scheme_arg (princ_name,fun_name,s) =
   Names.Id.print princ_name ++ str " :=" ++ spc() ++ str "Induction for " ++
   Libnames.pr_qualid fun_name ++ spc() ++ str "Sort " ++
   Termops.pr_sort_family s
 
+}
+
 VERNAC ARGUMENT EXTEND fun_scheme_arg
-PRINTED BY pr_fun_scheme_arg
-| [ ident(princ_name) ":=" "Induction" "for" reference(fun_name) "Sort" sort_family(s) ] -> [ (princ_name,fun_name,s) ]
+PRINTED BY { pr_fun_scheme_arg }
+| [ ident(princ_name) ":=" "Induction" "for" reference(fun_name) "Sort" sort_family(s) ] -> { (princ_name,fun_name,s) }
 END
 
+{
 
 let warning_error names e =
   let (e, _) = ExplainErr.process_vernac_interp_error (e, Exninfo.null) in
@@ -187,12 +221,13 @@ let warning_error names e =
        warn_cannot_define_principle (names,error)
     | _ -> raise e
 
+}
 
 VERNAC COMMAND EXTEND NewFunctionalScheme
-   ["Functional" "Scheme" ne_fun_scheme_arg_list_sep(fas,"with") ]
-   => [ Vernacexpr.VtSideff(List.map pi1 fas), Vernacexpr.VtLater ]
+| ["Functional" "Scheme" ne_fun_scheme_arg_list_sep(fas,"with") ]
+   => { Vernacexpr.VtSideff(List.map pi1 fas), Vernacexpr.VtLater }
    ->
-    [
+    {
       begin
 	try
 	  Functional_principles_types.build_scheme fas
@@ -220,17 +255,17 @@ VERNAC COMMAND EXTEND NewFunctionalScheme
 	      warning_error names e
       end
 
-    ]
+    }
 END
 (***** debug only ***)
 
 VERNAC COMMAND EXTEND NewFunctionalCase
-  ["Functional" "Case" fun_scheme_arg(fas) ]
-  => [ Vernacexpr.VtSideff[pi1 fas], Vernacexpr.VtLater ]
-  -> [ Functional_principles_types.build_case_scheme fas ]
+| ["Functional" "Case" fun_scheme_arg(fas) ]
+  => { Vernacexpr.VtSideff[pi1 fas], Vernacexpr.VtLater }
+  -> { Functional_principles_types.build_case_scheme fas }
 END
 
 (***** debug only ***)
 VERNAC COMMAND EXTEND GenerateGraph CLASSIFIED AS QUERY
-["Generate" "graph" "for" reference(c)] -> [ make_graph (Smartlocate.global_with_alias c) ]
+| ["Generate" "graph" "for" reference(c)] -> { make_graph (Smartlocate.global_with_alias c) }
 END