aboutsummaryrefslogtreecommitdiffhomepage
path: root/intf/vernacexpr.mli
diff options
context:
space:
mode:
Diffstat (limited to 'intf/vernacexpr.mli')
-rw-r--r--intf/vernacexpr.mli2
1 files changed, 1 insertions, 1 deletions
diff --git a/intf/vernacexpr.mli b/intf/vernacexpr.mli
index 3ffaca113..be7e59a2d 100644
--- a/intf/vernacexpr.mli
+++ b/intf/vernacexpr.mli
@@ -320,7 +320,7 @@ type vernac_expr =
bool * (* abstract instance *)
local_binder list * (* super *)
typeclass_constraint * (* instance name, class name, params *)
- constr_expr option * (* props *)
+ (bool * constr_expr) option * (* props *)
int option (* Priority *)
| VernacContext of local_binder list