diff options
| author | Emilio Jesus Gallego Arias | 2017-01-17 15:06:26 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2017-04-24 23:58:23 +0200 |
| commit | bf13037e9ca39da28fb648e5488ce56ef8a1f1e2 (patch) | |
| tree | e981dabe208b339db88188b7a5e89c53d77745a1 /intf/misctypes.mli | |
| parent | a9d151a31937724543d5269e72b0262c8764c46e (diff) | |
[location] Use located in misctypes.
Diffstat (limited to 'intf/misctypes.mli')
| -rw-r--r-- | intf/misctypes.mli | 12 |
1 files changed, 6 insertions, 6 deletions
diff --git a/intf/misctypes.mli b/intf/misctypes.mli index 33dc2a335c..0157800cdd 100644 --- a/intf/misctypes.mli +++ b/intf/misctypes.mli @@ -27,12 +27,12 @@ and intro_pattern_naming_expr = and 'constr intro_pattern_action_expr = | IntroWildcard | IntroOrAndPattern of 'constr or_and_intro_pattern_expr - | IntroInjection of (Loc.t * 'constr intro_pattern_expr) list - | IntroApplyOn of (Loc.t * 'constr) * (Loc.t * 'constr intro_pattern_expr) + | IntroInjection of ('constr intro_pattern_expr) Loc.located list + | IntroApplyOn of 'constr Loc.located * 'constr intro_pattern_expr Loc.located | IntroRewrite of bool and 'constr or_and_intro_pattern_expr = - | IntroOrPattern of (Loc.t * 'constr intro_pattern_expr) list list - | IntroAndPattern of (Loc.t * 'constr intro_pattern_expr) list + | IntroOrPattern of ('constr intro_pattern_expr) Loc.located list list + | IntroAndPattern of ('constr intro_pattern_expr) Loc.located list (** Move destination for hypothesis *) @@ -79,7 +79,7 @@ type 'a cast_type = type quantified_hypothesis = AnonHyp of int | NamedHyp of Id.t -type 'a explicit_bindings = (Loc.t * quantified_hypothesis * 'a) list +type 'a explicit_bindings = (quantified_hypothesis * 'a) Loc.located list type 'a bindings = | ImplicitBindings of 'a list @@ -99,7 +99,7 @@ type 'a and_short_name = 'a * Id.t Loc.located option type 'a or_by_notation = | AN of 'a - | ByNotation of (Loc.t * string * string option) + | ByNotation of (string * string option) Loc.located (* NB: the last string in [ByNotation] is actually a [Notation.delimiters], but this formulation avoids a useless dependency. *) |