diff options
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 16f0c0c92a..2a542e0ff2 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 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. *) diff --git a/intf/vernacexpr.mli b/intf/vernacexpr.mli index f018d59e6b..211d41bb05 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; } |