diff options
| author | Pierre-Marie Pédrot | 2017-05-19 10:48:30 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2017-05-19 10:48:30 +0200 |
| commit | 0a67131d9a63e26ea2ea85d9ed51d76d8464295e (patch) | |
| tree | 980727a88f63908ce1f25f317e43126a0d3d0ad8 /interp/notation.mli | |
| parent | 37e84b83739fec666264904bc06fd32b46b83140 (diff) | |
| parent | 9f11adda4bff194a3c6a66d573ce7001d4399886 (diff) | |
Merge branch 'master' into ltac2-hooks
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 2e92a00a8c..300480ff1c 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 *) |