diff options
| author |  Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-05-15 01:10:54 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-05-15 04:51:09 +0200 |
| commit | b643916aed4093eb7f21116aaef726cab561bc27 (patch) | |
| tree | be6c8aa8fe99ccec0cf9908d36c89abda47cac1f /interp/notation.mli | |
| parent | 8e6d03830e9c53f641626e29886eb07c705f7608 (diff) | |
[interp] [ast] Make raw_cases_pattern_expr private.
The type `raw_cases_pattern_expr` is used only in the interpretation
of notation patterns. Indeed, this should be a private type thus we
make it local to `Constrintern`; it makes no sense to expose it in the
public AST.
The patch is routine, except for the case used to interpret primitives
in patterns. We now return a `glob_constr` representing the raw
pattern, instead of the private raw pattern type. This could be
further refactored but have opted to be conservative here.
This patch is a refinement of b2953849b999d1c3b42c0f494b234f2a93ac7754
, see the commentaries there for more information about
`raw_cases_pattern_expr`.
Diffstat (limited to 'interp/notation.mli')
| -rw-r--r-- | interp/notation.mli | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/interp/notation.mli b/interp/notation.mli index 2e92a00a8..300480ff1 100644 --- a/interp/notation.mli +++ b/interp/notation.mli @@ -85,8 +85,10 @@ val declare_string_interpreter : scope_name -> required_module -> val interp_prim_token : Loc.t -> prim_token -> local_scopes -> glob_constr * (notation_location * scope_name option) + +(* This function returns a glob_const representing a pattern *) val interp_prim_token_cases_pattern_expr : Loc.t -> (global_reference -> unit) -> prim_token -> - local_scopes -> raw_cases_pattern_expr * (notation_location * scope_name option) + local_scopes -> glob_constr * (notation_location * scope_name option) (** Return the primitive token associated to a [term]/[cases_pattern]; raise [No_match] if no such token *) |