diff options
Diffstat (limited to 'interp/notation.mli')
| -rw-r--r-- | interp/notation.mli | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/interp/notation.mli b/interp/notation.mli index 7629d86e7..3f66f993a 100644 --- a/interp/notation.mli +++ b/interp/notation.mli @@ -84,8 +84,8 @@ val declare_string_interpreter : scope_name -> required_module -> val interp_prim_token : loc -> prim_token -> local_scopes -> glob_constr * (notation_location * scope_name option) -val interp_prim_token_cases_pattern : loc -> prim_token -> name -> - local_scopes -> cases_pattern * (notation_location * scope_name option) +val interp_prim_token_cases_pattern_expr : loc -> (global_reference -> unit) -> prim_token -> + local_scopes -> raw_cases_pattern_expr * (notation_location * scope_name option) (** Return the primitive token associated to a [term]/[cases_pattern]; raise [No_match] if no such token *) |