diff options
| author | Maxime Dénès | 2018-03-10 10:03:50 +0100 |
|---|---|---|
| committer | Maxime Dénès | 2018-03-10 10:03:50 +0100 |
| commit | 93a1c4786c9b17efdda025f754ad97376d61a9ba (patch) | |
| tree | 9ffa30a21f0d5b80aaeae66955e652f185929498 /intf/misctypes.ml | |
| parent | 5f989f48eaaf5e13568fce9849f40bc554ca0166 (diff) | |
| parent | 4af41a12a0e7e6b17d25a71568641bd03d5e1f94 (diff) | |
Merge PR #6831: [located] More work towards using CAst.t
Diffstat (limited to 'intf/misctypes.ml')
| -rw-r--r-- | intf/misctypes.ml | 12 |
1 files changed, 6 insertions, 6 deletions
diff --git a/intf/misctypes.ml b/intf/misctypes.ml index 54a4861d09..1eee3dfc79 100644 --- a/intf/misctypes.ml +++ b/intf/misctypes.ml @@ -35,12 +35,12 @@ and intro_pattern_naming_expr = and 'constr intro_pattern_action_expr = | IntroWildcard | IntroOrAndPattern of 'constr or_and_intro_pattern_expr - | IntroInjection of ('constr intro_pattern_expr) Loc.located list - | IntroApplyOn of 'constr Loc.located * 'constr intro_pattern_expr Loc.located + | IntroInjection of ('constr intro_pattern_expr) CAst.t list + | IntroApplyOn of 'constr CAst.t * 'constr intro_pattern_expr CAst.t | IntroRewrite of bool and 'constr or_and_intro_pattern_expr = - | IntroOrPattern of ('constr intro_pattern_expr) Loc.located list list - | IntroAndPattern of ('constr intro_pattern_expr) Loc.located list + | IntroOrPattern of ('constr intro_pattern_expr) CAst.t list list + | IntroAndPattern of ('constr intro_pattern_expr) CAst.t list (** Move destination for hypothesis *) @@ -95,7 +95,7 @@ type 'a cast_type = type quantified_hypothesis = AnonHyp of int | NamedHyp of Id.t -type 'a explicit_bindings = (quantified_hypothesis * 'a) Loc.located list +type 'a explicit_bindings = (quantified_hypothesis * 'a) CAst.t list type 'a bindings = | ImplicitBindings of 'a list @@ -115,7 +115,7 @@ type 'a and_short_name = 'a * lident option type 'a or_by_notation = | AN of 'a - | ByNotation of (string * string option) Loc.located + | ByNotation of (string * string option) CAst.t (* NB: the last string in [ByNotation] is actually a [Notation.delimiters], but this formulation avoids a useless dependency. *) |