From 8ca8b7766ff9c00a76094d63973e15c87e19a9d6 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Thu, 21 Jun 2018 16:20:35 +0200
Subject: [PATCH] handle language.of_val in solve_into_val
---
theories/heap_lang/tactics.v | 1 +
1 file changed, 1 insertion(+)
diff --git a/theories/heap_lang/tactics.v b/theories/heap_lang/tactics.v
index 1efe90f58..604a7244d 100644
--- a/theories/heap_lang/tactics.v
+++ b/theories/heap_lang/tactics.v
@@ -96,6 +96,7 @@ Ltac of_expr e :=
let e1 := of_expr e1 in let e2 := of_expr e2 in constr:(FAA e1 e2)
| to_expr ?e => e
| of_val ?v => constr:(Val v (of_val v) (to_of_val v))
+ | language.of_val ?v => constr:(Val v (of_val v) (to_of_val v))
| _ => match goal with
| H : to_val e = Some ?v |- _ => constr:(Val v e H)
| H : Closed [] e |- _ => constr:(@ClosedExpr e H)
--
GitLab