From 81c0aaee8a99878d81501cfe3f780146fe2ae1e6 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Tue, 10 May 2016 19:02:13 +0200
Subject: [PATCH] Make of_val reduce by simpl.

And make constants P for which we do not want of_val P to reduce Opaque.
---
 heap_lang/lib/barrier/barrier.v | 1 +
 heap_lang/lib/lock.v            | 1 +
 heap_lang/lib/par.v             | 2 +-
 heap_lang/lib/spawn.v           | 1 +
 heap_lang/substitution.v        | 1 -
 heap_lang/wp_tactics.v          | 4 ++--
 tests/barrier_client.v          | 1 +
 tests/heap_lang.v               | 1 +
 tests/joining_existentials.v    | 1 +
 tests/one_shot.v                | 1 +
 10 files changed, 10 insertions(+), 4 deletions(-)

diff --git a/heap_lang/lib/barrier/barrier.v b/heap_lang/lib/barrier/barrier.v
index d8e4a6618..b3b5902ff 100644
--- a/heap_lang/lib/barrier/barrier.v
+++ b/heap_lang/lib/barrier/barrier.v
@@ -4,3 +4,4 @@ Definition newbarrier : val := λ: <>, ref #0.
 Definition signal : val := λ: "x", '"x" <- #1.
 Definition wait : val :=
   rec: "wait" "x" := if: !'"x" = #1 then #() else '"wait" '"x".
+Global Opaque newbarrier signal wait.
diff --git a/heap_lang/lib/lock.v b/heap_lang/lib/lock.v
index b0707a29c..df476fbf4 100644
--- a/heap_lang/lib/lock.v
+++ b/heap_lang/lib/lock.v
@@ -8,6 +8,7 @@ Definition acquire : val :=
   rec: "acquire" "l" :=
     if: CAS '"l" #false #true then #() else '"acquire" '"l".
 Definition release : val := λ: "l", '"l" <- #false.
+Global Opaque newlock acquire release.
 
 (** The CMRA we need. *)
 (* Not bundling heapG, as it may be shared with other users. *)
diff --git a/heap_lang/lib/par.v b/heap_lang/lib/par.v
index 8f1812620..e394bfc47 100644
--- a/heap_lang/lib/par.v
+++ b/heap_lang/lib/par.v
@@ -14,7 +14,7 @@ Infix "||" := Par : expr_scope.
 Instance do_wexpr_par {X Y} (H : X `included` Y) : WExpr H par par := _.
 Instance do_wsubst_par {X Y} x es (H : X `included` x :: Y) :
   WSubst x es H par par := do_wsubst_closed _ x es H _.
-Typeclasses Opaque par.
+Global Opaque par.
 
 Section proof.
 Context {Σ : gFunctors} `{!heapG Σ, !spawnG Σ}.
diff --git a/heap_lang/lib/spawn.v b/heap_lang/lib/spawn.v
index 294325be7..b2f5f24be 100644
--- a/heap_lang/lib/spawn.v
+++ b/heap_lang/lib/spawn.v
@@ -13,6 +13,7 @@ Definition join : val :=
       InjR "x" => '"x"
     | InjL <>  => '"join" '"c"
     end.
+Global Opaque spawn join.
 
 (** The CMRA we need. *)
 (* Not bundling heapG, as it may be shared with other users. *)
diff --git a/heap_lang/substitution.v b/heap_lang/substitution.v
index 50b67fcc5..62d1b3d6d 100644
--- a/heap_lang/substitution.v
+++ b/heap_lang/substitution.v
@@ -196,4 +196,3 @@ Ltac simpl_subst :=
 Arguments wexpr : simpl never.
 Arguments subst : simpl never.
 Arguments wsubst : simpl never.
-Arguments of_val : simpl never.
diff --git a/heap_lang/wp_tactics.v b/heap_lang/wp_tactics.v
index 06e776156..2411087c3 100644
--- a/heap_lang/wp_tactics.v
+++ b/heap_lang/wp_tactics.v
@@ -9,7 +9,7 @@ Ltac wp_bind K :=
   | _ => etrans; [|fast_by apply (wp_bind K)]; simpl
   end.
 
-Ltac wp_done := rewrite -/of_val /= ?to_of_val; fast_done.
+Ltac wp_done := rewrite /= ?to_of_val; fast_done.
 
 Ltac wp_value_head :=
   match goal with
@@ -23,7 +23,7 @@ Ltac wp_value_head :=
   end.
 
 Ltac wp_finish := intros_revert ltac:(
-  rewrite -/of_val /= ?to_of_val; try strip_later; try wp_value_head).
+  rewrite /= ?to_of_val; try strip_later; try wp_value_head).
 
 Tactic Notation "wp_value" :=
   lazymatch goal with
diff --git a/tests/barrier_client.v b/tests/barrier_client.v
index 0338d3e07..ca07236f2 100644
--- a/tests/barrier_client.v
+++ b/tests/barrier_client.v
@@ -11,6 +11,7 @@ Definition client : expr [] :=
   let: "b" := ^newbarrier #() in
   ('"y" <- (λ: "z", '"z" + #42) ;; ^signal '"b") ||
     (^(worker 12) '"b" '"y" || ^(worker 17) '"b" '"y").
+Global Opaque worker client.
 
 Section client.
   Context {Σ : gFunctors} `{!heapG Σ, !barrierG Σ, !spawnG Σ} (heapN N : namespace).
diff --git a/tests/heap_lang.v b/tests/heap_lang.v
index 22cabb3ec..f83c8a8d7 100644
--- a/tests/heap_lang.v
+++ b/tests/heap_lang.v
@@ -37,6 +37,7 @@ Section LiftingTests.
   Definition Pred : val :=
     λ: "x",
       if: '"x" ≤ #0 then -^FindPred (-'"x" + #2) #0 else ^FindPred '"x" #0.
+  Global Opaque FindPred Pred.
 
   Lemma FindPred_spec n1 n2 E Φ :
     n1 < n2 →
diff --git a/tests/joining_existentials.v b/tests/joining_existentials.v
index 377ebcf52..969586fdf 100644
--- a/tests/joining_existentials.v
+++ b/tests/joining_existentials.v
@@ -7,6 +7,7 @@ Import uPred.
 Definition client eM eW1 eW2 : expr [] :=
   let: "b" := newbarrier #() in
   (eM ;; ^signal '"b") || ((^wait '"b" ;; eW1) || (^wait '"b" ;; eW2)).
+Global Opaque client.
 
 Section proof.
 Context (G : cFunctor).
diff --git a/tests/one_shot.v b/tests/one_shot.v
index a96ffa375..89dd05d94 100644
--- a/tests/one_shot.v
+++ b/tests/one_shot.v
@@ -18,6 +18,7 @@ Definition one_shot_example : val := λ: <>,
        | InjR "m" => Assert ('"n" = '"m")
        end
     end)).
+Global Opaque one_shot_example.
 
 Class one_shotG Σ :=
   OneShotG { one_shot_inG :> inG heap_lang Σ (one_shotR (dec_agreeR Z)) }.
-- 
GitLab