From 45a78bd3225d3a669006a89f2597e3878015299f Mon Sep 17 00:00:00 2001
From: Jacques-Henri Jourdan <jacques-henri.jourdan@normalesup.org>
Date: Tue, 27 Feb 2018 20:45:44 +0100
Subject: [PATCH] Comment.

---
 theories/proofmode/classes.v | 13 +++++++++----
 1 file changed, 9 insertions(+), 4 deletions(-)

diff --git a/theories/proofmode/classes.v b/theories/proofmode/classes.v
index 32b0d168c..acef2f557 100644
--- a/theories/proofmode/classes.v
+++ b/theories/proofmode/classes.v
@@ -389,10 +389,15 @@ Instance maybe_frame_default {PROP : bi} (R P : PROP) :
   TCOr (Affine R) (Absorbing P) → MaybeFrame false R P P false | 100.
 Proof. intros. rewrite /MaybeFrame /=. apply: sep_elim_r. Qed.
 
-(* For each of the [MakeXxxx] class, there is a [KnownMakeXxxx] variant,
-   that only succeeds if the parameter(s) is not an evar. In the case
-   the parameter(s) is an evar, then [MakeXxxx] will not instantiate
-   it arbitrarily. *)
+(* For each of the [MakeXxxx] class, there is a [KnownMakeXxxx]
+   variant, that only succeeds if the parameter(s) is not an evar. In
+   the case the parameter(s) is an evar, then [MakeXxxx] will not
+   instantiate it arbitrarily.
+
+   The reason for this is that if given an evar, these typeclasses
+   would typically try to instantiate this evar with some arbitrary
+   logical constructs such as emp or True. Therefore, we use an Hint
+   Mode to disable all the instances that would have this behavior. *)
 Class MakeEmbed `{BiEmbedding PROP PROP'} (P : PROP) (Q : PROP') :=
   make_embed : ⎡P⎤ ⊣⊢ Q.
 Arguments MakeEmbed {_ _ _ _} _%I _%I.
-- 
GitLab