From 41dd8385e9362fbf6f26f3fd9809cd051e2f9070 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Wed, 15 Feb 2017 21:15:37 +0100
Subject: [PATCH] Port Iris 84d78426: Remove an Ltac hack that was there for
unknown reason.
---
theories/lang/tactics.v | 3 +--
1 file changed, 1 insertion(+), 2 deletions(-)
diff --git a/theories/lang/tactics.v b/theories/lang/tactics.v
index 7ebfc8c5..299ae3f1 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 :=
--
GitLab