diff options
| -rw-r--r-- | interp/constrintern.ml | 2 | ||||
| -rw-r--r-- | test-suite/bugs/closed/4305.v | 17 |
2 files changed, 18 insertions, 1 deletions
diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 982d9bfe39..8c56d0ccfe 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -1120,7 +1120,7 @@ let drop_notations_pattern looked_for = let (argscs,_) = find_remaining_scopes pats [] g in Some (g, List.map2 (in_pat_sc env) argscs pats, []) | NApp (NRef g,args) -> - ensure_kind top loc g; + test_kind top g; let nvars = List.length vars in if List.length pats < nvars then error_not_enough_arguments loc; let pats1,pats2 = List.chop nvars pats in diff --git a/test-suite/bugs/closed/4305.v b/test-suite/bugs/closed/4305.v new file mode 100644 index 0000000000..39fc02d22b --- /dev/null +++ b/test-suite/bugs/closed/4305.v @@ -0,0 +1,17 @@ +(* Check fallback when an abbreviation is not interpretable as a pattern *) + +Notation foo := Type. + +Definition t := + match 0 with + | S foo => foo + | _ => 0 + end. + +Notation bar := (option Type). + +Definition u := + match 0 with + | S bar => bar + | _ => 0 + end. |