From db37c9f3f32ae7a2abcd5e1a3f6239eddb5e1768 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Mon, 23 Jun 2014 13:01:31 +0200
Subject: Fix semantics of change p with c to typecheck c at each specific
 occurrence of p, avoiding unwanted universe constraints in presence of
 universe polymorphic constants. Fixing HoTT bugs # 36, 54 and 113.

---
 plugins/romega/refl_omega.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'plugins/romega')

diff --git a/plugins/romega/refl_omega.ml b/plugins/romega/refl_omega.ml
index c5a0f798ce..e22816c136 100644
--- a/plugins/romega/refl_omega.ml
+++ b/plugins/romega/refl_omega.ml
@@ -1282,7 +1282,7 @@ let resolution env full_reified_goal systems_list =
 
   Tactics.generalize
     (l_generalize_arg @ List.map Term.mkVar (List.tl l_hyps)) >>
-  Tactics.change_in_concl None reified >>
+  Tactics.change_concl reified >>
   Tactics.apply (app coq_do_omega [|decompose_tactic; normalization_trace|]) >>
   show_goal >>
   Tactics.normalise_vm_in_concl >>
-- 
cgit v1.2.3