From ba2bdb733586f5ce34901ca988d7f5f559b53591 Mon Sep 17 00:00:00 2001
From: "Paolo G. Giarrusso" <p.giarrusso@gmail.com>
Date: Sat, 4 Apr 2020 21:05:17 +0200
Subject: [PATCH] Switch `inj _` to `inj f`, part 1

Code affected by a00d9bd814bc97622b2e9cf86c0a78e300680f70.
---
 theories/namespaces.v | 2 +-
 theories/option.v     | 4 ++--
 2 files changed, 3 insertions(+), 3 deletions(-)

diff --git a/theories/namespaces.v b/theories/namespaces.v
index 2d5038c0..9bd02fcd 100644
--- a/theories/namespaces.v
+++ b/theories/namespaces.v
@@ -58,7 +58,7 @@ Section namespace.
     intros Hxy a. unfold up_close. rewrite !nclose_eq, !ndot_eq.
     unfold nclose_def, ndot_def; rewrite !elem_coPset_suffixes.
     intros [qx ->] [qy Hqy].
-    revert Hqy. by intros [= ?%(inj _)]%positives_flatten_suffix_eq.
+    revert Hqy. by intros [= ?%(inj encode)]%positives_flatten_suffix_eq.
   Qed.
 
   Lemma ndot_preserve_disjoint_l N E x : ↑N ## E → ↑N.@x ## E.
diff --git a/theories/option.v b/theories/option.v
index f658505e..f8c284a9 100644
--- a/theories/option.v
+++ b/theories/option.v
@@ -189,8 +189,8 @@ Lemma fmap_Some_equiv {A B} `{Equiv B} `{!Equivalence (≡@{B})} (f : A → B) m
   f <$> mx ≡ Some y ↔ ∃ x, mx = Some x ∧ y ≡ f x.
 Proof.
   destruct mx; simpl; split.
-  - intros ?%(inj _). eauto.
-  - intros (? & ->%(inj _) & ?). constructor. done.
+  - intros ?%(inj Some). eauto.
+  - intros (? & ->%(inj Some) & ?). constructor. done.
   - intros ?%symmetry%equiv_None. done.
   - intros (? & ? & ?). done.
 Qed.
-- 
GitLab