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, 0 insertions, 164 deletions

diff --git a/plugins/firstorder/g_ground.ml4 b/plugins/firstorder/g_ground.ml4
deleted file mode 100644
index db753fc672..0000000000
--- a/plugins/firstorder/g_ground.ml4
+++ /dev/null
@@ -1,164 +0,0 @@
-(************************************************************************)
-(*         *   The Coq Proof Assistant / The Coq Development Team       *)
-(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
-(* <O___,, *       (see CREDITS file for the list of authors)           *)
-(*   \VV/  **************************************************************)
-(*    //   *    This file is distributed under the terms of the         *)
-(*         *     GNU Lesser General Public License Version 2.1          *)
-(*         *     (see LICENSE file for the text of the license)         *)
-(************************************************************************)
-
-
-open Ltac_plugin
-open Formula
-open Sequent
-open Ground
-open Goptions
-open Tacmach.New
-open Tacticals.New
-open Tacinterp
-open Stdarg
-open Tacarg
-open Pcoq.Prim
-
-DECLARE PLUGIN "ground_plugin"
-
-(* declaring search depth as a global option *)
-
-let ground_depth=ref 3
-
-let _=
-  let gdopt=
-    { optdepr=false;
-      optname="Firstorder Depth";
-      optkey=["Firstorder";"Depth"];
-      optread=(fun ()->Some !ground_depth);
-      optwrite=
-   (function
-	None->ground_depth:=3
-      |	Some i->ground_depth:=(max i 0))}
-  in
-    declare_int_option gdopt
-
-
-let _=
-  let congruence_depth=ref 100 in
-  let gdopt=
-    { optdepr=true; (* noop *)
-      optname="Congruence Depth";
-      optkey=["Congruence";"Depth"];
-      optread=(fun ()->Some !congruence_depth);
-      optwrite=
-   (function
-        None->congruence_depth:=0
-      |	Some i->congruence_depth:=(max i 0))}
-  in
-    declare_int_option gdopt
-
-let default_intuition_tac =
-  let tac _ _ = Auto.h_auto None [] None in
-  let name = { Tacexpr.mltac_plugin = "ground_plugin"; mltac_tactic = "auto_with"; } in
-  let entry = { Tacexpr.mltac_name = name; mltac_index = 0 } in
-  Tacenv.register_ml_tactic name [| tac |];
-  Tacexpr.TacML (Loc.tag (entry, []))
-
-let (set_default_solver, default_solver, print_default_solver) = 
-  Tactic_option.declare_tactic_option ~default:default_intuition_tac "Firstorder default solver"
-
-VERNAC COMMAND FUNCTIONAL EXTEND Firstorder_Set_Solver CLASSIFIED AS SIDEFF
-| [ "Set" "Firstorder" "Solver" tactic(t) ] -> [
-    fun ~atts ~st -> let open Vernacinterp in
-      set_default_solver
-        (Locality.make_section_locality atts.locality)
-        (Tacintern.glob_tactic t);
-        st
-  ]
-END
-
-VERNAC COMMAND EXTEND Firstorder_Print_Solver CLASSIFIED AS QUERY
-| [ "Print" "Firstorder" "Solver" ] -> [
-    Feedback.msg_info
-      (Pp.(++) (Pp.str"Firstorder solver tactic is ") (print_default_solver ())) ]
-END
-
-let fail_solver=tclFAIL 0 (Pp.str "GTauto failed")
-
-let gen_ground_tac flag taco ids bases =
-  let backup= !qflag in
-  Proofview.tclOR begin
-  Proofview.Goal.enter begin fun gl ->
-      qflag:=flag;
-      let solver=
-	match taco with
-	    Some tac-> tac
-	  | None-> snd (default_solver ()) in
-      let startseq k =
-        Proofview.Goal.enter begin fun gl ->
-	let seq=empty_seq !ground_depth in
-        let seq, sigma = extend_with_ref_list (pf_env gl) (project gl) ids seq in
-        let seq, sigma = extend_with_auto_hints (pf_env gl) (project gl) bases seq in
-        tclTHEN (Proofview.Unsafe.tclEVARS sigma) (k seq)
-        end
-      in
-      let result=ground_tac solver startseq in
-      qflag := backup;
-      result
-  end
-  end
-  (fun (e, info) -> qflag := backup; Proofview.tclZERO ~info e)
-
-(* special for compatibility with Intuition
-
-let constant str = Coqlib.get_constr str
-
-let defined_connectives=lazy
-  [[],EvalConstRef (destConst (constant "core.not.type"));
-   [],EvalConstRef (destConst (constant "core.iff.type"))]
-
-let normalize_evaluables=
-  onAllHypsAndConcl
-    (function
-	 None->unfold_in_concl (Lazy.force defined_connectives)
-       | Some id->
-	   unfold_in_hyp (Lazy.force defined_connectives)
-	   (Tacexpr.InHypType id)) *)
-
-open Ppconstr
-open Printer
-let pr_firstorder_using_raw _ _ _ = Pptactic.pr_auto_using pr_qualid
-let pr_firstorder_using_glob _ _ _ = Pptactic.pr_auto_using (pr_or_var (fun x -> pr_global (snd x)))
-let pr_firstorder_using_typed _ _ _ = Pptactic.pr_auto_using pr_global
-
-let warn_deprecated_syntax =
-  CWarnings.create ~name:"firstorder-deprecated-syntax" ~category:"deprecated"
-    (fun () -> Pp.strbrk "Deprecated syntax; use \",\" as separator")
-
-
-ARGUMENT EXTEND firstorder_using
-  TYPED AS reference_list
-  PRINTED BY pr_firstorder_using_typed
-  RAW_PRINTED BY pr_firstorder_using_raw
-  GLOB_PRINTED BY pr_firstorder_using_glob
-| [ "using" reference(a) ] -> [ [a] ]
-| [ "using" reference(a) "," ne_reference_list_sep(l,",") ] -> [ a::l ]
-| [ "using" reference(a) reference(b) reference_list(l) ] -> [
-    warn_deprecated_syntax ();
-    a::b::l
-  ]
-| [ ] -> [ [] ]
-END
-
-TACTIC EXTEND firstorder
-    [ "firstorder" tactic_opt(t) firstorder_using(l) ] ->
-      [ gen_ground_tac true (Option.map (tactic_of_value ist) t) l [] ]
-|   [ "firstorder" tactic_opt(t) "with" ne_preident_list(l) ] ->
-      [ gen_ground_tac true (Option.map (tactic_of_value ist) t) [] l ]
-|   [ "firstorder" tactic_opt(t) firstorder_using(l)
-       "with" ne_preident_list(l') ] ->
-      [ gen_ground_tac true (Option.map (tactic_of_value ist) t) l l' ]
-END
-
-TACTIC EXTEND gintuition
-  [ "gintuition" tactic_opt(t) ] ->
-     [ gen_ground_tac false (Option.map (tactic_of_value ist) t) [] [] ]
-END