From 967088a6f87405a93ce21971392c58996df8c99f Mon Sep 17 00:00:00 2001
From: Georges Gonthier
Date: Mon, 19 Nov 2018 17:35:52 +0100
Subject: 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)
---
 plugin/v8.6/ssrfun.v | 6 ++++--
 1 file changed, 4 insertions(+), 2 deletions(-)

(limited to 'plugin')

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     *)
-- 
cgit v1.2.3