diff --git a/theories/heap_lang/tactics.v b/theories/heap_lang/tactics.v
index 1c040a9472665570c95a71ed86f0c904d8ba720c..92765fd945f219b18298fc87e776127444bc2801 100644
--- a/theories/heap_lang/tactics.v
+++ b/theories/heap_lang/tactics.v
@@ -91,8 +91,7 @@ Ltac of_expr e :=
      constr:(CAS e0 e1 e2)
   | to_expr ?e => e
   | of_val ?v => constr:(Val v)
-  | _ => constr:(ltac:(
-     match goal with H : Closed [] e |- _ => exact (@ClosedExpr e H) end))
+  | _ => match goal with H : Closed [] e |- _ => constr:(@ClosedExpr e H) end
   end.
 
 Fixpoint is_closed (X : list string) (e : expr) : bool :=