Split the firstorder plugin into a core package and an Ltac1 syntax.

Alizter · Jul 4, 2024 · 2ffdf62 · 2ffdf62
1 parent 270eb2b
commit 2ffdf62
Show file tree

Hide file tree

Showing 7 changed files with 19 additions and 9 deletions.
diff --git a/lib/core_plugins_findlib_compat.ml b/lib/core_plugins_findlib_compat.ml
@@ -11,6 +11,7 @@
 let legacy_to_findlib = [
   ("btauto_plugin",                 ["plugins";"btauto"]) ;
   ("derive_plugin",                 ["plugins";"derive"]) ;
+  ("firstorder_core_plugin",        ["plugins";"firstorder_core"]) ;
   ("firstorder_plugin",             ["plugins";"firstorder"]) ;
   ("ltac_plugin",                   ["plugins";"ltac"]) ;
   ("micromega_core_plugin",         ["plugins";"micromega_core";]) ;

diff --git a/plugins/firstorder/dune b/plugins/firstorder/dune
@@ -1,7 +1,16 @@
+(library
+ (name firstorder_core_plugin)
+ (public_name coq-core.plugins.firstorder_core)
+ (synopsis "Coq's first order logic solver plugin")
+ (modules (:standard \ g_ground))
+ (libraries coq-core.tactics))
+
 (library
  (name firstorder_plugin)
  (public_name coq-core.plugins.firstorder)
- (synopsis "Coq's first order logic solver plugin")
- (libraries coq-core.plugins.ltac))
+ (synopsis "Coq's first order logic solver plugin (Ltac1 syntax)")
+ (flags :standard -open Firstorder_core_plugin)
+ (modules g_ground)
+ (libraries coq-core.plugins.firstorder_core coq-core.plugins.ltac))
 
 (coq.pp (modules g_ground))
diff --git a/plugins/firstorder/firstorder_core_plugin.mllib b/plugins/firstorder/firstorder_core_plugin.mllib
diff --git a/plugins/firstorder/g_ground.mlg b/plugins/firstorder/g_ground.mlg
@@ -80,6 +80,11 @@ let gen_ground_tac flag taco ids bases =
         tclTHEN (Proofview.Unsafe.tclEVARS sigma) (k seq)
         end
       in
+      let () =
+        if Tacinterp.get_debug()=Tactic_debug.DebugOn 0
+        then
+          Feedback.msg_debug (Printer.Debug.pr_goal gl)
+      in
       let result=ground_tac ~flags solver startseq in
       result
   end

diff --git a/plugins/firstorder/ground.ml b/plugins/firstorder/ground.ml
@@ -8,7 +8,6 @@
 (*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
-open Ltac_plugin
 open Formula
 open Sequent
 open Rules
@@ -31,11 +30,6 @@ let ground_tac ~flags solver startseq =
   Proofview.Goal.enter begin fun gl ->
   let rec toptac skipped seq =
     Proofview.Goal.enter begin fun gl ->
-    let () =
-      if Tacinterp.get_debug()=Tactic_debug.DebugOn 0
-      then
-        Feedback.msg_debug (Printer.Debug.pr_goal gl)
-    in
     tclORELSE (axiom_tac seq)
       begin
         try

diff --git a/theories/Init/Prelude.v b/theories/Init/Prelude.v
@@ -28,6 +28,7 @@ Require Export Coq.Init.Tauto.
 *)
 Declare ML Module "cc_core_plugin:coq-core.plugins.cc_core".
 Declare ML Module "cc_plugin:coq-core.plugins.cc".
+Declare ML Module "firstorder_core_plugin:coq-core.plugins.firstorder_core".
 Declare ML Module "firstorder_plugin:coq-core.plugins.firstorder".
 
 (* Parsing / printing of hexadecimal numbers *)

diff --git a/tools/dune_rule_gen/coq_rules.ml b/tools/dune_rule_gen/coq_rules.ml
@@ -37,7 +37,7 @@ module FlagUtil = struct
 
   let findlib_plugin_fixup p =
     ["number_string_notation"; "zify"; "tauto"; "ssreflect";
-      "cc_core"; "micromega_core"]
+      "cc_core"; "firstorder_core"; "micromega_core"]
     @ (List.filter (fun s -> not (String.equal s "syntax" || String.equal s "ssr")) p)
 
   (* This can also go when the -I flags are gone, by passing the meta