From 84d784267e8a03ab7b2db5f1d75a269e52f8d151 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Tue, 14 Feb 2017 17:13:38 +0100
Subject: [PATCH] Remove an Ltac hack that was there for unknown reason.
---
theories/heap_lang/tactics.v | 3 +--
1 file changed, 1 insertion(+), 2 deletions(-)
diff --git a/theories/heap_lang/tactics.v b/theories/heap_lang/tactics.v
index 1c040a947..92765fd94 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 :=
--
GitLab