From a2b62737f76788dd8598c6352419675a7410fca5 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Wed, 27 Jul 2016 16:39:07 +0200
Subject: [PATCH] don't backtrace on the operator
---
heap_lang/wp_tactics.v | 2 +-
1 file changed, 1 insertion(+), 1 deletion(-)
diff --git a/heap_lang/wp_tactics.v b/heap_lang/wp_tactics.v
index 361b83a3a..e84f90afe 100644
--- a/heap_lang/wp_tactics.v
+++ b/heap_lang/wp_tactics.v
@@ -82,7 +82,7 @@ Tactic Notation "wp_seq" := wp_let.
Tactic Notation "wp_op" :=
lazymatch goal with
| |- _ ⊢ wp ?E ?e ?Q => reshape_expr e ltac:(fun K e' =>
- match eval hnf in e' with
+ lazymatch eval hnf in e' with
| BinOp LtOp _ _ => wp_bind K; apply wp_lt; wp_finish
| BinOp LeOp _ _ => wp_bind K; apply wp_le; wp_finish
| BinOp EqOp _ _ => wp_bind K; apply wp_eq; wp_finish
--
GitLab