diff options
| author |  Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-04-08 23:19:35 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-04-25 00:32:37 +0200 |
| commit | 054d2736c1c1b55cb7708ff0444af521cd0fe2ba (patch) | |
| tree | 5228705fd054a59afec759eec780d2b4e9b53435 /intf | |
| parent | d062642d6e3671bab8a0e6d70e346325558d2db3 (diff) | |
[location] [ast] Switch Constrexpr AST to an extensible node type.
Following @gasche idea, and the original intention of #402, we switch
the main parsing AST of Coq from `'a Loc.located` to `'a CAst.ast`
which is private and record-based.
This provides significantly clearer code for the AST, and is robust
wrt attributes.
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 23223173e..4f1e9d8e6 100644 --- a/intf/constrexpr.mli +++ b/intf/constrexpr.mli @@ -42,7 +42,7 @@ type raw_cases_pattern_expr_r = (** [CPatCstr (_, c, l1, l2)] represents ((@c l1) l2) *) | RCPatAtom of Id.t option | RCPatOr of raw_cases_pattern_expr list -and raw_cases_pattern_expr = raw_cases_pattern_expr_r Loc.located +and raw_cases_pattern_expr = raw_cases_pattern_expr_r CAst.ast type instance_expr = Misctypes.glob_level list @@ -61,7 +61,7 @@ type cases_pattern_expr_r = | CPatRecord of (reference * cases_pattern_expr) list | CPatDelimiters of string * cases_pattern_expr | CPatCast of cases_pattern_expr * constr_expr -and cases_pattern_expr = cases_pattern_expr_r Loc.located +and cases_pattern_expr = cases_pattern_expr_r CAst.ast and cases_pattern_notation_substitution = cases_pattern_expr list * (** for constr subterms *) @@ -98,7 +98,7 @@ and constr_expr_r = | CGeneralization of binding_kind * abstraction_kind option * constr_expr | CPrim of prim_token | CDelimiters of string * constr_expr -and constr_expr = constr_expr_r Loc.located +and constr_expr = constr_expr_r CAst.ast and case_expr = constr_expr (* expression that is being matched *) * Name.t Loc.located option (* as-clause *) |