diff options
Diffstat (limited to 'plugins/romega/g_romega.mlg')
-rw-r--r-- | plugins/romega/g_romega.mlg | 63 |
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 |