aboutsummaryrefslogtreecommitdiff
path: root/intf/constrexpr.mli
diff options
context:
space:
mode:
Diffstat (limited to 'intf/constrexpr.mli')
-rw-r--r--intf/constrexpr.mli6
1 files changed, 3 insertions, 3 deletions
diff --git a/intf/constrexpr.mli b/intf/constrexpr.mli
index c1ea71df43..92d0020a5d 100644
--- a/intf/constrexpr.mli
+++ b/intf/constrexpr.mli
@@ -125,9 +125,9 @@ and recursion_order_expr =
(** Anonymous defs allowed ?? *)
and local_binder_expr =
- | CLocalAssum of Name.t located list * binder_kind * constr_expr
- | CLocalDef of Name.t located * constr_expr * constr_expr option
- | CLocalPattern of Loc.t * cases_pattern_expr * constr_expr option
+ | CLocalAssum of Name.t located list * binder_kind * constr_expr
+ | CLocalDef of Name.t located * constr_expr * constr_expr option
+ | CLocalPattern of (cases_pattern_expr * constr_expr option) Loc.located
and constr_notation_substitution =
constr_expr list * (** for constr subterms *)