1 files changed, 4 insertions, 4 deletions
diff --git a/src/Util/Tactics/UnifyAbstractReflexivity.v b/src/Util/Tactics/UnifyAbstractReflexivity.v
index 687518377..e3e7fc77b 100644
--- a/src/Util/Tactics/UnifyAbstractReflexivity.v
+++ b/src/Util/Tactics/UnifyAbstractReflexivity.v
@@ -15,10 +15,10 @@ Ltac unify_transformed_rhs_abstract_tac transform_rhs unify exact_no_check :=
   lazymatch goal with
   | [ |- ?LHS = ?RHS ]
     => tryif has_evar LHS
-    then let RHS' := transform_rhs RHS in
-         unify LHS RHS'; clear;
-         abstract exact_no_check (eq_refl RHS')
-    else abstract exact_no_check (eq_refl RHS)
+    then (let RHS' := transform_rhs RHS in
+          unify LHS RHS'; clear;
+          abstract exact_no_check (eq_refl RHS'))
+    else (abstract exact_no_check (eq_refl RHS))
   end.
 
 Ltac idterm x := x.