From 4c39126f0a0a97152f67a3a5e7c86db860f48e39 Mon Sep 17 00:00:00 2001
From: Pierre Roux
Date: Fri, 24 Apr 2020 21:52:37 +0200
Subject: 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)
---
 interp/constrextern.ml | 11 +++--------
 1 file changed, 3 insertions(+), 8 deletions(-)

(limited to 'interp/constrextern.ml')

diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index a37bac3275..d5a5bde616 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -435,13 +435,10 @@ let extern_record_pattern cstrsp args =
 let rec extern_cases_pattern_in_scope (custom,scopes as allscopes) vars pat =
   try
     if !Flags.in_debugger || !Flags.raw_print || !print_no_symbol then raise No_match;
-    let (na,sc,p) = uninterp_prim_token_cases_pattern pat in
+    let (na,p,key) = uninterp_prim_token_cases_pattern pat scopes in
     match availability_of_entry_coercion custom InConstrEntrySomeLevel with
       | None -> raise No_match
       | Some coercion ->
-    match availability_of_prim_token p sc scopes with
-      | None -> raise No_match
-      | Some key ->
         let loc = cases_pattern_loc pat in
         insert_pat_coercion ?loc coercion
           (insert_pat_alias ?loc (insert_pat_delimiters ?loc (CAst.make ?loc @@ CPatPrim p) key) na)
@@ -848,13 +845,11 @@ let same_binder_type ty nal c =
 (* one with no delimiter if possible)                                 *)
 
 let extern_possible_prim_token (custom,scopes) r =
-   let (sc,n) = uninterp_prim_token r in
+   let (n,key) = uninterp_prim_token r scopes in
    match availability_of_entry_coercion custom InConstrEntrySomeLevel with
    | None -> raise No_match
    | Some coercion ->
-   match availability_of_prim_token n sc scopes with
-   | None -> raise No_match
-   | Some key -> insert_entry_coercion coercion (insert_delimiters (CAst.make ?loc:(loc_of_glob_constr r) @@ CPrim n) key)
+      insert_entry_coercion coercion (insert_delimiters (CAst.make ?loc:(loc_of_glob_constr r) @@ CPrim n) key)
 
 let filter_enough_applied nargs l =
   match nargs with
-- 
cgit v1.2.3