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/micromega/coq_micromega.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'plugins/micromega')

diff --git a/plugins/micromega/coq_micromega.ml b/plugins/micromega/coq_micromega.ml
index d11454b276..ebd0420226 100644
--- a/plugins/micromega/coq_micromega.ml
+++ b/plugins/micromega/coq_micromega.ml
@@ -1378,7 +1378,7 @@ let micromega_order_change spec cert cert_typ env ff gl =
  let formula_typ = (Term.mkApp (Lazy.force coq_Cstr,[|spec.coeff|])) in
  let ff = dump_formula formula_typ (dump_cstr spec.coeff spec.dump_coeff) ff in
  let vm = dump_varmap (spec.typ) env in
-  Tactics.change_in_concl None
+  Tactics.change_concl
    (set
      [
       ("__ff", ff, Term.mkApp(Lazy.force coq_Formula, [|formula_typ |]));
@@ -1666,7 +1666,7 @@ let micromega_order_changer cert env ff gl =
  let formula_typ = (Term.mkApp (Lazy.force coq_Cstr,[| coeff|])) in
  let ff = dump_formula formula_typ (dump_cstr coeff dump_coeff) ff in
  let vm = dump_varmap (typ) env in
-  Tactics.change_in_concl None
+  Tactics.change_concl
    (set
      [
       ("__ff", ff, Term.mkApp(Lazy.force coq_Formula, [|formula_typ |]));
-- 
cgit v1.2.3