From 9f4e0d61abb3dd65943cc8242a4c7b0556d42757 Mon Sep 17 00:00:00 2001
From: Jason Gross <jgross@mit.edu>
Date: Mon, 23 Jan 2017 17:43:22 -0500
Subject: Preserve names in invert_expr_subst

---
 src/Reflection/ExprInversion.v | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

(limited to 'src')

diff --git a/src/Reflection/ExprInversion.v b/src/Reflection/ExprInversion.v
index 8604a089d..1130570a9 100644
--- a/src/Reflection/ExprInversion.v
+++ b/src/Reflection/ExprInversion.v
@@ -147,10 +147,11 @@ Ltac invert_expr_subst_step :=
   | [ e : expr _ _ (Arrow _ _) |- _ ]
     => let f := fresh e in
        let H := fresh in
-       remember (invert_Abs e) as f eqn:H;
+       rename e into f;
+       remember (invert_Abs f) as e eqn:H;
        symmetry in H;
        apply invert_Abs_Some in H;
-       subst e
+       subst f
   | [ H : invert_Abs ?e = _ |- _ ] => apply invert_Abs_Some in H
   | [ H : invert_Return ?e = _ |- _ ] => apply invert_Return_Some in H
   | _ => progress subst
-- 
cgit v1.2.3