From cb485174b737578d496f70829b85444d09143267 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Tue, 10 May 2016 15:10:59 +0200
Subject: [PATCH] Turn some matches into lazymatches so errors propagate
 properly.

---
 heap_lang/proofmode.v  | 12 ++++++------
 heap_lang/wp_tactics.v | 14 +++++++-------
 2 files changed, 13 insertions(+), 13 deletions(-)

diff --git a/heap_lang/proofmode.v b/heap_lang/proofmode.v
index 086fdd294..abb497d4f 100644
--- a/heap_lang/proofmode.v
+++ b/heap_lang/proofmode.v
@@ -86,14 +86,14 @@ Qed.
 End heap.
 
 Tactic Notation "wp_apply" open_constr(lem) :=
-  match goal with
+  lazymatch goal with
   | |- _ ⊢ wp ?E ?e ?Q => reshape_expr e ltac:(fun K e' =>
     wp_bind K; iApply lem; try iNext)
   | _ => fail "wp_apply: not a 'wp'"
   end.
 
 Tactic Notation "wp_alloc" ident(l) "as" constr(H) :=
-  match goal with
+  lazymatch goal with
   | |- _ ⊢ wp ?E ?e ?Q => reshape_expr e ltac:(fun K e' =>
     match eval hnf in e' with
     | Alloc ?e =>
@@ -112,7 +112,7 @@ Tactic Notation "wp_alloc" ident(l) :=
   let H := iFresh in wp_alloc l as H.
 
 Tactic Notation "wp_load" :=
-  match goal with
+  lazymatch goal with
   | |- _ ⊢ wp ?E ?e ?Q => reshape_expr e ltac:(fun K e' =>
     match eval hnf in e' with
     | Load (Lit (LitLoc ?l)) =>
@@ -127,7 +127,7 @@ Tactic Notation "wp_load" :=
   end.
 
 Tactic Notation "wp_store" :=
-  match goal with
+  lazymatch goal with
   | |- _ ⊢ wp ?E ?e ?Q => reshape_expr e ltac:(fun K e' =>
     match eval hnf in e' with
     | Store ?l ?e =>
@@ -144,7 +144,7 @@ Tactic Notation "wp_store" :=
   end.
 
 Tactic Notation "wp_cas_fail" :=
-  match goal with
+  lazymatch goal with
   | |- _ ⊢ wp ?E ?e ?Q => reshape_expr e ltac:(fun K e' =>
     match eval hnf in e' with
     | CAS ?l ?e1 ?e2 =>
@@ -162,7 +162,7 @@ Tactic Notation "wp_cas_fail" :=
   end.
 
 Tactic Notation "wp_cas_suc" :=
-  match goal with
+  lazymatch goal with
   | |- _ ⊢ wp ?E ?e ?Q => reshape_expr e ltac:(fun K e' =>
     match eval hnf in e' with
     | CAS ?l ?e1 ?e2 =>
diff --git a/heap_lang/wp_tactics.v b/heap_lang/wp_tactics.v
index 7f3763606..9ebb7bb3d 100644
--- a/heap_lang/wp_tactics.v
+++ b/heap_lang/wp_tactics.v
@@ -26,7 +26,7 @@ Ltac wp_finish := intros_revert ltac:(
   rewrite -/of_val /= ?to_of_val; try strip_later; try wp_value_head).
 
 Tactic Notation "wp_value" :=
-  match goal with
+  lazymatch goal with
   | |- _ ⊢ wp ?E ?e ?Q => reshape_expr e ltac:(fun K e' =>
     wp_bind K; wp_value_head) || fail "wp_value: cannot find value in" e
   | _ => fail "wp_value: not a wp"
@@ -44,7 +44,7 @@ Tactic Notation "wp_rec" :=
   end.
 
 Tactic Notation "wp_lam" :=
-  match goal with
+  lazymatch goal with
   | |- _ ⊢ wp ?E ?e ?Q => reshape_expr e ltac:(fun K e' =>
     match eval hnf in e' with App ?e1 _ =>
 (*    match eval hnf in e1 with Rec BAnon _ _ => *)
@@ -57,7 +57,7 @@ Tactic Notation "wp_let" := wp_lam.
 Tactic Notation "wp_seq" := wp_let.
 
 Tactic Notation "wp_op" :=
-  match goal with
+  lazymatch goal with
   | |- _ ⊢ wp ?E ?e ?Q => reshape_expr e ltac:(fun K e' =>
     match eval hnf in e' with
     | BinOp LtOp _ _ => wp_bind K; apply wp_lt; wp_finish
@@ -72,7 +72,7 @@ Tactic Notation "wp_op" :=
   end.
 
 Tactic Notation "wp_proj" :=
-  match goal with
+  lazymatch goal with
   | |- _ ⊢ wp ?E ?e ?Q => reshape_expr e ltac:(fun K e' =>
     match eval hnf in e' with
     | Fst _ => wp_bind K; etrans; [|eapply wp_fst; wp_done]; wp_finish
@@ -82,7 +82,7 @@ Tactic Notation "wp_proj" :=
   end.
 
 Tactic Notation "wp_if" :=
-  match goal with
+  lazymatch goal with
   | |- _ ⊢ wp ?E ?e ?Q => reshape_expr e ltac:(fun K e' =>
     match eval hnf in e' with
     | If _ _ _ =>
@@ -93,7 +93,7 @@ Tactic Notation "wp_if" :=
   end.
 
 Tactic Notation "wp_case" :=
-  match goal with
+  lazymatch goal with
   | |- _ ⊢ wp ?E ?e ?Q => reshape_expr e ltac:(fun K e' =>
     match eval hnf in e' with
     | Case _ _ _ =>
@@ -105,7 +105,7 @@ Tactic Notation "wp_case" :=
   end.
 
 Tactic Notation "wp_focus" open_constr(efoc) :=
-  match goal with
+  lazymatch goal with
   | |- _ ⊢ wp ?E ?e ?Q => reshape_expr e ltac:(fun K e' =>
     match e' with
     | efoc => unify e' efoc; wp_bind K
-- 
GitLab