aboutsummaryrefslogtreecommitdiff
path: root/test-suite/output/ErrorInModule.v
diff options
context:
space:
mode:
authorEmilio Jesus Gallego Arias2017-05-15 01:10:54 +0200
committerEmilio Jesus Gallego Arias2017-05-15 04:51:09 +0200
commitb643916aed4093eb7f21116aaef726cab561bc27 (patch)
treebe6c8aa8fe99ccec0cf9908d36c89abda47cac1f /test-suite/output/ErrorInModule.v
parent8e6d03830e9c53f641626e29886eb07c705f7608 (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 'test-suite/output/ErrorInModule.v')
0 files changed, 0 insertions, 0 deletions