diff options
Diffstat (limited to 'plugins/romega/g_romega.ml4')
| -rw-r--r-- | plugins/romega/g_romega.ml4 | 20 |
1 files changed, 10 insertions, 10 deletions
diff --git a/plugins/romega/g_romega.ml4 b/plugins/romega/g_romega.ml4 index 830dc54d..5b77d08d 100644 --- a/plugins/romega/g_romega.ml4 +++ b/plugins/romega/g_romega.ml4 @@ -6,28 +6,28 @@ *************************************************************************) -(*i camlp4deps: "grammar/grammar.cma" i*) DECLARE PLUGIN "romega_plugin" +open Ltac_plugin open Names open Refl_omega -open Constrarg +open Stdarg let eval_tactic name = let dp = DirPath.make (List.map Id.of_string ["PreOmega"; "omega"; "Coq"]) in - let kn = KerName.make2 (MPfile dp) (Label.make name) 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 l = +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.error ("No ROmega knowledge base for type "^s)) + | s -> CErrors.user_err Pp.(str ("No ROmega knowledge base for type "^s))) (Util.List.sort_uniquize String.compare l) in Tacticals.New.tclTHEN @@ -37,15 +37,15 @@ let romega_tactic l = we'd better leave as little as possible in the conclusion, for an easier decidability argument. *) (Tactics.intros) - (Proofview.V82.tactic total_reflexive_omega_tactic)) - + (total_reflexive_omega_tactic unsafe)) TACTIC EXTEND romega -| [ "romega" ] -> [ romega_tactic [] ] +| [ "romega" ] -> [ romega_tactic false [] ] +| [ "unsafe_romega" ] -> [ romega_tactic true [] ] END TACTIC EXTEND romega' | [ "romega" "with" ne_ident_list(l) ] -> - [ romega_tactic (List.map Names.Id.to_string l) ] -| [ "romega" "with" "*" ] -> [ romega_tactic ["nat";"positive";"N";"Z"] ] + [ romega_tactic false (List.map Names.Id.to_string l) ] +| [ "romega" "with" "*" ] -> [ romega_tactic false ["nat";"positive";"N";"Z"] ] END |