From 28db0f239f18f3ecfb37ac302529773a1d8ac064 Mon Sep 17 00:00:00 2001
From: letouzey
Date: Fri, 24 Mar 2006 22:55:59 +0000
Subject: utilisation de la VM pour la normalisation finale de romega

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8660 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 contrib/romega/refl_omega.ml | 8 +++++++-
 1 file changed, 7 insertions(+), 1 deletion(-)

diff --git a/contrib/romega/refl_omega.ml b/contrib/romega/refl_omega.ml
index 99fafd2638..285fc0ca8c 100644
--- a/contrib/romega/refl_omega.ml
+++ b/contrib/romega/refl_omega.ml
@@ -1318,7 +1318,13 @@ let resolution env full_reified_goal systems_list =
   Tactics.change_in_concl None reified >> 
   Tactics.apply (app coq_do_omega [|decompose_tactic; normalization_trace|]) >>
   show_goal >>
-  Tactics.normalise_in_concl >>
+  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: 
+      Tacmach.convert_concl_no_check (Lazy.force coq_True) Term.VMcast >> 
+  i*)
   Tactics.apply (Lazy.force coq_I)
 
 let total_reflexive_omega_tactic gl = 
-- 
cgit v1.2.3