aboutsummaryrefslogtreecommitdiffhomepage
path: root/toplevel/vernacexpr.ml
diff options
context:
space:
mode:
Diffstat (limited to 'toplevel/vernacexpr.ml')
-rw-r--r--toplevel/vernacexpr.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/toplevel/vernacexpr.ml b/toplevel/vernacexpr.ml
index beb26e41f..441244caf 100644
--- a/toplevel/vernacexpr.ml
+++ b/toplevel/vernacexpr.ml
@@ -125,7 +125,7 @@ type inductive_flag = bool (* true = Inductive; false = CoInductive *)
type sort_expr = Rawterm.rawsort
-type decl_notation = (string * scope_name option) option
+type decl_notation = (string * constr_expr * scope_name option) option
type simple_binder = identifier * constr_expr
type 'a with_coercion = coercion_flag * 'a
type constructor_expr = simple_binder with_coercion