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.

2 files changed, 16 insertions, 16 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
diff --git a/plugins/romega/refl_omega.ml b/plugins/romega/refl_omega.ml
index 7b63d5503..7a48b9788 100644
--- a/plugins/romega/refl_omega.ml
+++ b/plugins/romega/refl_omega.ml
@@ -974,7 +974,7 @@ l'extraction d'un ensemble minimal de solutions permettant la
 résolution globale du système et enfin construit la trace qui permet
 de faire rejouer cette solution par la tactique réflexive. *)
 
-let resolution env (reified_concl,reified_hyps) systems_list =
+let resolution unsafe env (reified_concl,reified_hyps) systems_list =
   let num = ref 0 in
   let solve_system list_eq =
     let index = !num in
@@ -1070,16 +1070,16 @@ let resolution env (reified_concl,reified_hyps) systems_list =
   Tactics.change_concl (EConstr.of_constr reified) >>
   Tactics.apply (EConstr.of_constr (app coq_do_omega [|decompose_tactic|])) >>
   show_goal >>
-  Tactics.normalise_vm_in_concl >>
-  (*i Alternatives to the previous line:
-   - Normalisation without VM:
-      Tactics.normalise_in_concl
-   - Skip the conversion check and rely directly on the QED:
-      Tactics.convert_concl_no_check (Lazy.force coq_True) Term.VMcast >>
-  i*)
+  (if unsafe then
+     (* Trust the produced term. Faster, but might fail later at Qed.
+        Also handy when debugging, e.g. via a Show Proof after romega. *)
+     Tactics.convert_concl_no_check
+       (EConstr.of_constr (Lazy.force coq_True)) Term.VMcast
+   else
+     Tactics.normalise_vm_in_concl) >>
   Tactics.apply (EConstr.of_constr (Lazy.force coq_I))
 
-let total_reflexive_omega_tactic =
+let total_reflexive_omega_tactic unsafe =
   Proofview.Goal.nf_enter { enter = begin fun gl ->
   Coqlib.check_required_library ["Coq";"romega";"ROmega"];
   rst_omega_eq ();
@@ -1090,7 +1090,7 @@ let total_reflexive_omega_tactic =
   let full_reified_goal = (id_concl,Pnot concl) :: hyps in
   let systems_list = destructurate_hyps full_reified_goal in
   if !debug then display_systems systems_list;
-  resolution env reified_goal systems_list
+  resolution unsafe env reified_goal systems_list
   with NO_CONTRADICTION -> CErrors.error "ROmega can't solve this system"
   end }