aboutsummaryrefslogtreecommitdiff
path: root/intf
diff options
context:
space:
mode:
Diffstat (limited to 'intf')
-rw-r--r--intf/constrexpr.mli2
1 files changed, 1 insertions, 1 deletions
diff --git a/intf/constrexpr.mli b/intf/constrexpr.mli
index 49bafadc8e..a4a6eb9092 100644
--- a/intf/constrexpr.mli
+++ b/intf/constrexpr.mli
@@ -19,7 +19,7 @@ open Decl_kinds
type notation = string
type explicitation =
- | ExplByPos of int * Id.t option
+ | ExplByPos of int * Id.t option (* a reference to the n-th product starting from left *)
| ExplByName of Id.t
type binder_kind =