Improve documentation of phant_id usage

Point out the use of id/idfun to control printing of notation.
(as suggested by @anton-trunov - see #247)

1 files changed, 4 insertions, 2 deletions

diff --git a/plugin/v8.6/ssrfun.v b/plugin/v8.6/ssrfun.v
index 7cb30ff..edee109 100644
--- a/plugin/v8.6/ssrfun.v
+++ b/plugin/v8.6/ssrfun.v
@@ -74,8 +74,10 @@ Require Import ssreflect.
 (*   Definition foo T sT & T -> sort sT := ...                                *)
 (* We can avoid specifying sT directly by calling foo (@id T), or specify     *)
 (* the call completely while still ensuring the consistency of T and sT, by   *)
-(* calling @foo T sT idfun. The phant_id type allows us to extend this trick  *)
-(* to non-Type canonical projections. It also allows us to sidestep           *)
+(* calling @foo T sT idfun; using different terms for the identity function   *)
+(* in the two use cases lets Coq print different Notation for each case.      *)
+(*   The phant_id type allows us to extend the phant structure inference      *)
+(* trick to non-Type canonical projections. It also allows us to sidestep     *)
 (* dependent type constraints when building explicit records, e.g., given     *)
 (*    Record r := R {x; y : T(x)}.                                            *)
 (* if we need to build an r from a given y0 while inferring some x0, such     *)