diff options
| author | Pierre Roux | 2020-04-24 21:52:37 +0200 |
|---|---|---|
| committer | Pierre Roux | 2020-05-02 20:37:50 +0200 |
| commit | 4c39126f0a0a97152f67a3a5e7c86db860f48e39 (patch) | |
| tree | 568955642bf955fb03e51f364d3561dbd681440f /interp/notation.mli | |
| parent | cacb6fed6dea278f46f83c1657f4a8c3c98817db (diff) | |
Fix #12159 (Numeral Notations do not play well with multiple scopes for the same inductive)
Numeral Notations now play better with multiple scopes for the same
inductive. Previously, when multiple numeral notations where defined
for the same inductive, only the last one was considered for
printing. Now, we proceed as follows
1. keep only uninterpreters that produce an output (first
List.map_filter)
2. keep only uninterpretation for scopes that either have a scope
delimiter or are open (second List.map_filter)
3. the final selection is made according to the order of open scopes,
(find_uninterpretation) or or according to the last defined
notation if no appropriate scope is open (head of list at the end)
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 892eba8d11..842f2b1458 100644 --- a/interp/notation.mli +++ b/interp/notation.mli @@ -206,9 +206,9 @@ val interp_prim_token_cases_pattern_expr : ?loc:Loc.t -> (GlobRef.t -> unit) -> raise [No_match] if no such token *) val uninterp_prim_token : - 'a glob_constr_g -> scope_name * prim_token + 'a glob_constr_g -> subscopes -> prim_token * delimiters option val uninterp_prim_token_cases_pattern : - 'a cases_pattern_g -> Name.t * scope_name * prim_token + 'a cases_pattern_g -> subscopes -> Name.t * prim_token * delimiters option val availability_of_prim_token : prim_token -> scope_name -> subscopes -> delimiters option option |