Skip to content
Snippets Groups Projects
Commit 41dd8385 authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Port Iris 84d78426: Remove an Ltac hack that was there for unknown reason.

parent 855e5e45
No related branches found
No related tags found
No related merge requests found
......@@ -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 :=
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment