romega: add a tactic named unsafe_romega (for debugging, or bold users)

 In this variant, the proof term produced by romega isn't verified at
 the tactic run-time (no vm_compute). In theory, [unsafe_romega] should
 behave exactly as [romega], but faster. Now, if there's a bug in romega,
 we'll be notified only at the following Qed. This could be interesting
 for debugging purpose : you could inspect the produced buggish term
 via a Show Proof.

1 files changed, 6 insertions, 6 deletions

diff --git a/plugins/romega/g_romega.ml4 b/plugins/romega/g_romega.ml4
index df7e5cb99..c2d7d5050 100644
--- a/plugins/romega/g_romega.ml4
+++ b/plugins/romega/g_romega.ml4
@@ -21,7 +21,7 @@ let eval_tactic name =
   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"
@@ -38,15 +38,15 @@ let romega_tactic l =
           we'd better leave as little as possible in the conclusion,
           for an easier decidability argument. *)
        (Tactics.intros)
-       (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