From 1773697769488de3fe56a9627ad1a40386059463 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Sat, 27 Feb 2016 19:28:05 +0100
Subject: [PATCH] =?UTF-8?q?Replace=20occurences=20of=20->=20by=20=E2=86=92?=
 =?UTF-8?q?.?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 algebra/cofe.v          | 2 +-
 algebra/upred.v         | 2 +-
 barrier/specification.v | 2 +-
 heap_lang/lang.v        | 2 +-
 4 files changed, 4 insertions(+), 4 deletions(-)

diff --git a/algebra/cofe.v b/algebra/cofe.v
index ce23c17d1..f3f680d11 100644
--- a/algebra/cofe.v
+++ b/algebra/cofe.v
@@ -54,7 +54,7 @@ Record CofeMixin A `{Equiv A, Compl A} := {
   mixin_dist_S n x y : x ≡{S n}≡ y → x ≡{n}≡ y;
   mixin_conv_compl n c : compl c ≡{n}≡ c (S n)
 }.
-Class Contractive `{Dist A, Dist B} (f : A -> B) :=
+Class Contractive `{Dist A, Dist B} (f : A → B) :=
   contractive n x y : (∀ i, i < n → x ≡{i}≡ y) → f x ≡{n}≡ f y.
 
 (** Bundeled version *)
diff --git a/algebra/upred.v b/algebra/upred.v
index 7fd9b5bff..e462a32a9 100644
--- a/algebra/upred.v
+++ b/algebra/upred.v
@@ -85,7 +85,7 @@ Lemma uPred_map_compose {M1 M2 M3 : cmraT} (f : M1 -n> M2) (g : M2 -n> M3)
 Proof. by split=> n x Hx. Qed.
 Lemma uPred_map_ext {M1 M2 : cmraT} (f g : M1 -n> M2)
       `{!CMRAMonotone f} `{!CMRAMonotone g}:
-  (∀ x, f x ≡ g x) -> ∀ x, uPred_map f x ≡ uPred_map g x.
+  (∀ x, f x ≡ g x) → ∀ x, uPred_map f x ≡ uPred_map g x.
 Proof. intros Hf P; split=> n x Hx /=; by rewrite /uPred_holds /= Hf. Qed.
 Definition uPredC_map {M1 M2 : cmraT} (f : M2 -n> M1) `{!CMRAMonotone f} :
   uPredC M1 -n> uPredC M2 := CofeMor (uPred_map f : uPredC M1 → uPredC M2).
diff --git a/barrier/specification.v b/barrier/specification.v
index 06c20b034..3bd06c46d 100644
--- a/barrier/specification.v
+++ b/barrier/specification.v
@@ -11,7 +11,7 @@ Local Notation iProp := (iPropG heap_lang Σ).
 (* TODO: Maybe notation for LocV (and Loc)? *)
 Lemma barrier_spec (heapN N : namespace) :
   heapN ⊥ N →
-  ∃ recv send : loc -> iProp -n> iProp,
+  ∃ recv send : loc → iProp -n> iProp,
     (∀ P, heap_ctx heapN ⊑ {{ True }} newchan '() {{ λ v, ∃ l, v = LocV l ★ recv l P ★ send l P }}) ∧
     (∀ l P, {{ send l P ★ P }} signal (LocV l) {{ λ _, True }}) ∧
     (∀ l P, {{ recv l P }} wait (LocV l) {{ λ _, P }}) ∧
diff --git a/heap_lang/lang.v b/heap_lang/lang.v
index 5c7555fc8..9c106a1d6 100644
--- a/heap_lang/lang.v
+++ b/heap_lang/lang.v
@@ -183,7 +183,7 @@ Definition bin_op_eval (op : bin_op) (l1 l2 : base_lit) : option base_lit :=
   | _, _, _ => None
   end.
 
-Inductive head_step : expr -> state -> expr -> state -> option expr -> Prop :=
+Inductive head_step : expr → state → expr → state → option expr → Prop :=
   | BetaS f x e1 e2 v2 σ :
      to_val e2 = Some v2 →
      head_step (App (Rec f x e1) e2) σ
-- 
GitLab