diff options
| -rw-r--r-- | interp/constrextern.ml | 13 | ||||
| -rw-r--r-- | test-suite/output/Notations2.out | 2 | ||||
| -rw-r--r-- | test-suite/output/Notations2.v | 7 |
3 files changed, 19 insertions, 3 deletions
diff --git a/interp/constrextern.ml b/interp/constrextern.ml index 237ffb55b..91a9eeefa 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -555,9 +555,16 @@ let rec remove_coercions inctx = function let l = list_skipn n args in let (a,l) = match l with a::l -> (a,l) | [] -> assert false in (* Recursively remove the head coercions *) - (match remove_coercions true a with - | RApp (_,a,l') -> RApp (loc,a,l'@l) - | a -> RApp (loc,a,l)) + let a' = remove_coercions true a in + (* Don't flatten App's in case of funclass so that + (atomic) notations on [a] work; should be compatible + since printer does not care whether App's are + collapsed or not and notations with an implicit + coercion using funclass either would have already + been confused with ordinary application or would have need + a surrounding context and the coercion to funclass would + have been made explicit to match *) + if l = [] then a' else RApp (loc,a',l) | _ -> c with Not_found -> c) | c -> c diff --git a/test-suite/output/Notations2.out b/test-suite/output/Notations2.out new file mode 100644 index 000000000..8a18a9d85 --- /dev/null +++ b/test-suite/output/Notations2.out @@ -0,0 +1,2 @@ +2 3 + : PAIR diff --git a/test-suite/output/Notations2.v b/test-suite/output/Notations2.v new file mode 100644 index 000000000..039771d5d --- /dev/null +++ b/test-suite/output/Notations2.v @@ -0,0 +1,7 @@ +(**********************************************************************) +(* Test call to primitive printers in presence of coercion to *) +(* functions (cf bug #2044) *) + +Inductive PAIR := P (n1:nat) (n2:nat). +Coercion P : nat >-> Funclass. +Check (2 3). |