From 98960cbeda9aadce25e7cf9731d11691582a7e63 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Fri, 13 Feb 2015 10:09:18 -0800
Subject: [PATCH] fix(library/tactic/rewrite_tactic): bug in HoTT mode

---
 src/library/tactic/rewrite_tactic.cpp | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/library/tactic/rewrite_tactic.cpp b/src/library/tactic/rewrite_tactic.cpp
index 9ed386c0e..561ce1788 100644
--- a/src/library/tactic/rewrite_tactic.cpp
+++ b/src/library/tactic/rewrite_tactic.cpp
@@ -993,7 +993,7 @@ class rewrite_fn {
             expr M   = m_g.mk_meta(m_ngen.next(), Pb);
             expr H;
             if (has_dep_elim) {
-                expr Haeqx = mk_app(mk_constant(get_eq_name(), {l1}), A, b, mk_var(0));
+                expr Haeqx = mk_app(mk_constant(get_eq_name(), {l2}), A, b, mk_var(0));
                 expr P     = mk_lambda("x", A, mk_lambda("H", Haeqx, Px));
                 H          = mk_app({mk_constant(get_eq_rec_name(), {l1, l2}), A, b, P, M, a, Heq});
             } else {