diff options
| author |  Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-01-17 15:06:26 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-04-24 23:58:23 +0200 |
| commit | bf13037e9ca39da28fb648e5488ce56ef8a1f1e2 (patch) | |
| tree | e981dabe208b339db88188b7a5e89c53d77745a1 /intf | |
| parent | a9d151a31937724543d5269e72b0262c8764c46e (diff) | |
[location] Use located in misctypes.
Diffstat (limited to 'intf')
| -rw-r--r-- | intf/genredexpr.mli | 2 | ||||
| -rw-r--r-- | intf/misctypes.mli | 12 | ||||
| -rw-r--r-- | intf/vernacexpr.mli | 2 |
3 files changed, 8 insertions, 8 deletions
diff --git a/intf/genredexpr.mli b/intf/genredexpr.mli index 16f0c0c92..2a542e0ff 100644 --- a/intf/genredexpr.mli +++ b/intf/genredexpr.mli @@ -52,7 +52,7 @@ type ('a,'b,'c) red_expr_gen = type ('a,'b,'c) may_eval = | ConstrTerm of 'a | ConstrEval of ('a,'b,'c) red_expr_gen * 'a - | ConstrContext of (Loc.t * Id.t) * 'a + | ConstrContext of Id.t Loc.located * 'a | ConstrTypeOf of 'a open Libnames diff --git a/intf/misctypes.mli b/intf/misctypes.mli index 33dc2a335..0157800cd 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. *) diff --git a/intf/vernacexpr.mli b/intf/vernacexpr.mli index f018d59e6..211d41bb0 100644 --- a/intf/vernacexpr.mli +++ b/intf/vernacexpr.mli @@ -482,7 +482,7 @@ and vernac_implicit_status = Implicit | MaximallyImplicit | NotImplicit and vernac_argument_status = { name : Name.t; recarg_like : bool; - notation_scope : (Loc.t * string) option; + notation_scope : string Loc.located option; implicit_status : vernac_implicit_status; } |