diff options
| author |  Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-01-17 14:44:28 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-04-24 23:58:23 +0200 |
| commit | a9d151a31937724543d5269e72b0262c8764c46e (patch) | |
| tree | c88761514ebb3b4ff2691acf8dcfec6f13135d97 /intf | |
| parent | 158f40db9482ead89befbf9bc9ad45ff8a60b75f (diff) | |
[location] More located use.
Diffstat (limited to 'intf')
| -rw-r--r-- | intf/constrexpr.mli | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/intf/constrexpr.mli b/intf/constrexpr.mli index c1ea71df4..92d0020a5 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 *) |