diff --git a/theories/lang/tactics.v b/theories/lang/tactics.v
index 7ebfc8c5e1f8b48e8c9b3668f79e216f8e868400..299ae3f1bbcb83d9fc95239315ca0c4d3c033c99 100644
--- a/theories/lang/tactics.v
+++ b/theories/lang/tactics.v
@@ -67,8 +67,7 @@ Ltac of_expr e :=
     let e := of_expr e in let el := of_expr el in constr:(e::el)
   | 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 :=