diff options
| -rw-r--r-- | interp/constrextern.ml | 10 | ||||
| -rw-r--r-- | test-suite/output/Notations4.out | 2 | ||||
| -rw-r--r-- | test-suite/output/Notations4.v | 4 |
3 files changed, 14 insertions, 2 deletions
diff --git a/interp/constrextern.ml b/interp/constrextern.ml index 601099c6ff..838ef40545 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -480,6 +480,9 @@ and apply_notation_to_pattern ?loc gr ((subst,substlist),(nb_to_drop,more_args)) (make_pat_notation ?loc ntn (l,ll) l2') key) end | SynDefRule kn -> + match availability_of_entry_coercion custom InConstrEntrySomeLevel with + | None -> raise No_match + | Some coercion -> let qid = Nametab.shortest_qualid_of_syndef ?loc vars kn in let l1 = List.rev_map (fun (c,(subentry,(scopt,scl))) -> @@ -493,7 +496,7 @@ and apply_notation_to_pattern ?loc gr ((subst,substlist),(nb_to_drop,more_args)) |None -> raise No_match in assert (List.is_empty substlist); - mkPat ?loc qid (List.rev_append l1 l2') + insert_pat_coercion ?loc coercion (mkPat ?loc qid (List.rev_append l1 l2')) and extern_notation_pattern allscopes vars t = function | [] -> raise No_match | (keyrule,pat,n as _rule)::rules -> @@ -1131,12 +1134,15 @@ and extern_notation (custom,scopes as allscopes) vars t = function binderlists in insert_coercion coercion (insert_delimiters (make_notation loc ntn (l,ll,bl,bll)) key)) | SynDefRule kn -> + match availability_of_entry_coercion custom InConstrEntrySomeLevel with + | None -> raise No_match + | Some coercion -> let l = List.map (fun (c,(subentry,(scopt,scl))) -> extern true (subentry,(scopt,scl@snd scopes)) vars c, None) terms in let a = CRef (Nametab.shortest_qualid_of_syndef ?loc vars kn,None) in - CAst.make ?loc @@ if List.is_empty l then a else CApp ((None, CAst.make a),l) in + insert_coercion coercion (CAst.make ?loc @@ if List.is_empty l then a else CApp ((None, CAst.make a),l)) in if List.is_empty args then e else let args = fill_arg_scopes args argsscopes allscopes in diff --git a/test-suite/output/Notations4.out b/test-suite/output/Notations4.out index cef7d1a702..46784d1897 100644 --- a/test-suite/output/Notations4.out +++ b/test-suite/output/Notations4.out @@ -1,5 +1,7 @@ [< 0 > + < 1 > * < 2 >] : nat +[< b > + < b > * < 2 >] + : nat [<< # 0 >>] : option nat [1 {f 1}] diff --git a/test-suite/output/Notations4.v b/test-suite/output/Notations4.v index 9738ce5a5e..6bdbf1bed5 100644 --- a/test-suite/output/Notations4.v +++ b/test-suite/output/Notations4.v @@ -10,6 +10,10 @@ Notation "x * y" := (Nat.mul x y) (in custom myconstr at level 4). Notation "< x >" := x (in custom myconstr at level 3, x constr at level 10). Check [ < 0 > + < 1 > * < 2 >]. +Axiom a : nat. +Notation b := a. +Check [ < b > + < a > * < 2 >]. + Declare Custom Entry anotherconstr. Notation "[ x ]" := x (x custom myconstr at level 6). |