diff options
Diffstat (limited to 'plugin')
| -rw-r--r-- | plugin/v8.6/ssrfun.v | 6 |
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 *) |