1 files changed, 63 insertions, 0 deletions
diff --git a/plugins/romega/g_romega.mlg b/plugins/romega/g_romega.mlg
new file mode 100644
index 00000000..ac4f30b1
--- /dev/null
+++ b/plugins/romega/g_romega.mlg
@@ -0,0 +1,63 @@
+(*************************************************************************
+
+   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))
+
+let romega_depr =
+  Vernacinterp.mk_deprecation
+    ~since:(Some "8.9")
+    ~note:(Some "Use lia instead.")
+    ()
+
+}
+
+TACTIC EXTEND romega
+DEPRECATED { romega_depr }
+|  [ "romega" ] -> { romega_tactic false [] }
+|  [ "unsafe_romega" ] -> { romega_tactic true [] }
+END
+
+TACTIC EXTEND romega'
+DEPRECATED { romega_depr }
+| [ "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