diff --git a/algebra/cofe.v b/algebra/cofe.v index ce23c17d1b308fab599e96f7e9f6509d37a91c77..f3f680d113a59335845ce71148f5a6e4dab2c1b3 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 7fd9b5bffb4bfa0fc51023a11ce18d6aafec6c8d..e462a32a92d2fa3f10a296046be71e8c0c2e4cb2 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 06c20b0342914bb088e292222e1f2bb31adc1c20..3bd06c46da4e084951ab21ba60c8ae4a610c2ea2 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 5c7555fc88c0e3b606671d29dee5edd7123ac4ef..9c106a1d668d144f143ee4728851df0321ac2a75 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) σ