From af2d7dea20d7a071407f9ac0d79b4f7b388b5299 Mon Sep 17 00:00:00 2001
From: Jacques-Henri Jourdan <jacques-henri.jourdan@normalesup.org>
Date: Tue, 23 Jan 2018 10:52:02 +0100
Subject: [PATCH] MakeMorphism -> MakeEmbed.

---
 theories/proofmode/class_instances.v | 20 ++++++++++----------
 1 file changed, 10 insertions(+), 10 deletions(-)

diff --git a/theories/proofmode/class_instances.v b/theories/proofmode/class_instances.v
index 9eb3cbd06..452615abe 100644
--- a/theories/proofmode/class_instances.v
+++ b/theories/proofmode/class_instances.v
@@ -805,23 +805,23 @@ Proof.
   rewrite /FromPure /Frame=> <-. by rewrite affinely_persistently_if_elim sep_elim_l.
 Qed.
 
-Class MakeMorphism `{BiEmbedding PROP PROP'} P (Q : PROP') :=
+Class MakeEmbed `{BiEmbedding PROP PROP'} P (Q : PROP') :=
   make_embed : ⎡P⎤ ⊣⊢ Q.
-Arguments MakeMorphism {_ _ _} _%I _%I.
+Arguments MakeEmbed {_ _ _} _%I _%I.
 Global Instance make_embed_pure `{BiEmbedding PROP PROP'} φ :
-  MakeMorphism ⌜φ⌝ ⌜φ⌝.
-Proof. by rewrite /MakeMorphism bi_embed_pure. Qed.
+  MakeEmbed ⌜φ⌝ ⌜φ⌝.
+Proof. by rewrite /MakeEmbed bi_embed_pure. Qed.
 Global Instance make_embed_emp `{BiEmbedding PROP PROP'} :
-  MakeMorphism emp emp.
-Proof. by rewrite /MakeMorphism bi_embed_emp. Qed.
+  MakeEmbed emp emp.
+Proof. by rewrite /MakeEmbed bi_embed_emp. Qed.
 Global Instance make_embed_default `{BiEmbedding PROP PROP'} :
-  MakeMorphism P ⎡P⎤ | 100.
-Proof. by rewrite /MakeMorphism. Qed.
+  MakeEmbed P ⎡P⎤ | 100.
+Proof. by rewrite /MakeEmbed. Qed.
 
 Global Instance frame_embed `{BiEmbedding PROP PROP'} p P Q (Q' : PROP') R :
-  Frame p R P Q → MakeMorphism Q Q' → Frame p ⎡R⎤ ⎡P⎤ Q'.
+  Frame p R P Q → MakeEmbed Q Q' → Frame p ⎡R⎤ ⎡P⎤ Q'.
 Proof.
-  rewrite /Frame /MakeMorphism => <- <-.
+  rewrite /Frame /MakeEmbed => <- <-.
   rewrite bi_embed_sep bi_embed_affinely_if bi_embed_persistently_if => //.
 Qed.
 
-- 
GitLab