From 682368d0b8a4211dbeba8c2423f53d0448fd7d71 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>
Date: Mon, 2 Jul 2018 16:14:05 +0200
Subject: Moving various ml4 files to mlg.

---
 plugins/romega/g_romega.ml4 | 51 -----------------------------------------
 plugins/romega/g_romega.mlg | 55 +++++++++++++++++++++++++++++++++++++++++++++
 2 files changed, 55 insertions(+), 51 deletions(-)
 delete mode 100644 plugins/romega/g_romega.ml4
 create mode 100644 plugins/romega/g_romega.mlg

(limited to 'plugins/romega')

diff --git a/plugins/romega/g_romega.ml4 b/plugins/romega/g_romega.ml4
deleted file mode 100644
index 5b77d08de..000000000
--- a/plugins/romega/g_romega.ml4
+++ /dev/null
@@ -1,51 +0,0 @@
-(*************************************************************************
-
-   PROJET RNRT Calife - 2001
-   Author: Pierre Crégut - France Télécom R&D
-   Licence : LGPL version 2.1
-
- *************************************************************************)
-
-
-DECLARE PLUGIN "romega_plugin"
-
-open Ltac_plugin
-open Names
-open Refl_omega
-open Stdarg
-
-let eval_tactic name =
-  let dp = DirPath.make (List.map Id.of_string ["PreOmega"; "omega"; "Coq"]) in
-  let kn = KerName.make2 (ModPath.MPfile dp) (Label.make name) in
-  let tac = Tacenv.interp_ltac kn in
-  Tacinterp.eval_tactic tac
-
-let romega_tactic unsafe l =
-  let tacs = List.map
-    (function
-       | "nat" -> eval_tactic "zify_nat"
-       | "positive" -> eval_tactic "zify_positive"
-       | "N" -> eval_tactic "zify_N"
-       | "Z" -> eval_tactic "zify_op"
-       | s -> CErrors.user_err Pp.(str ("No ROmega knowledge base for type "^s)))
-    (Util.List.sort_uniquize String.compare l)
-  in
-  Tacticals.New.tclTHEN
-    (Tacticals.New.tclREPEAT (Proofview.tclPROGRESS (Tacticals.New.tclTHENLIST tacs)))
-    (Tacticals.New.tclTHEN
-       (* because of the contradiction process in (r)omega,
-          we'd better leave as little as possible in the conclusion,
-          for an easier decidability argument. *)
-       (Tactics.intros)
-       (total_reflexive_omega_tactic unsafe))
-
-TACTIC EXTEND romega
-|  [ "romega" ] -> [ romega_tactic false [] ]
-|  [ "unsafe_romega" ] -> [ romega_tactic true [] ]
-END
-
-TACTIC EXTEND romega'
-| [ "romega" "with" ne_ident_list(l) ] ->
-    [ romega_tactic false (List.map Names.Id.to_string l) ]
-| [ "romega" "with" "*" ] -> [ romega_tactic false ["nat";"positive";"N";"Z"] ]
-END
diff --git a/plugins/romega/g_romega.mlg b/plugins/romega/g_romega.mlg
new file mode 100644
index 000000000..c1ce30027
--- /dev/null
+++ b/plugins/romega/g_romega.mlg
@@ -0,0 +1,55 @@
+(*************************************************************************
+
+   PROJET RNRT Calife - 2001
+   Author: Pierre Crégut - France Télécom R&D
+   Licence : LGPL version 2.1
+
+ *************************************************************************)
+
+
+DECLARE PLUGIN "romega_plugin"
+
+{
+
+open Ltac_plugin
+open Names
+open Refl_omega
+open Stdarg
+
+let eval_tactic name =
+  let dp = DirPath.make (List.map Id.of_string ["PreOmega"; "omega"; "Coq"]) in
+  let kn = KerName.make2 (ModPath.MPfile dp) (Label.make name) in
+  let tac = Tacenv.interp_ltac kn in
+  Tacinterp.eval_tactic tac
+
+let romega_tactic unsafe l =
+  let tacs = List.map
+    (function
+       | "nat" -> eval_tactic "zify_nat"
+       | "positive" -> eval_tactic "zify_positive"
+       | "N" -> eval_tactic "zify_N"
+       | "Z" -> eval_tactic "zify_op"
+       | s -> CErrors.user_err Pp.(str ("No ROmega knowledge base for type "^s)))
+    (Util.List.sort_uniquize String.compare l)
+  in
+  Tacticals.New.tclTHEN
+    (Tacticals.New.tclREPEAT (Proofview.tclPROGRESS (Tacticals.New.tclTHENLIST tacs)))
+    (Tacticals.New.tclTHEN
+       (* because of the contradiction process in (r)omega,
+          we'd better leave as little as possible in the conclusion,
+          for an easier decidability argument. *)
+       (Tactics.intros)
+       (total_reflexive_omega_tactic unsafe))
+
+}
+
+TACTIC EXTEND romega
+|  [ "romega" ] -> { romega_tactic false [] }
+|  [ "unsafe_romega" ] -> { romega_tactic true [] }
+END
+
+TACTIC EXTEND romega'
+| [ "romega" "with" ne_ident_list(l) ] ->
+    { romega_tactic false (List.map Names.Id.to_string l) }
+| [ "romega" "with" "*" ] -> { romega_tactic false ["nat";"positive";"N";"Z"] }
+END
-- 
cgit v1.2.3