diff options
| -rw-r--r-- | interp/constrintern.ml | 8 | ||||
| -rw-r--r-- | interp/syntax_def.ml | 7 | ||||
| -rw-r--r-- | interp/syntax_def.mli | 3 | ||||
| -rw-r--r-- | test-suite/bugs/closed/bug_9166.v | 9 |
4 files changed, 24 insertions, 3 deletions
diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 40922b5c35..7aa85a0810 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -1527,8 +1527,8 @@ let drop_notations_pattern looked_for genv = try match Nametab.locate_extended qid with | SynDef sp -> - let (vars,a) = Syntax_def.search_syntactic_definition sp in - (match a with + let filter (vars,a) = + try match a with | NRef g -> (* Convention: do not deactivate implicit arguments and scopes for further arguments *) test_kind top g; @@ -1549,7 +1549,9 @@ let drop_notations_pattern looked_for genv = let idspl1 = List.map (in_not false qid.loc scopes (subst, Id.Map.empty) []) args in let (_,argscs) = find_remaining_scopes pats1 pats2 g in Some (g, idspl1, List.map2 (in_pat_sc scopes) argscs pats2) - | _ -> raise Not_found) + | _ -> raise Not_found + with Not_found -> None in + Syntax_def.search_filtered_syntactic_definition filter sp | TrueGlobal g -> test_kind top g; Dumpglob.add_glob ?loc:qid.loc g; diff --git a/interp/syntax_def.ml b/interp/syntax_def.ml index b73d238c22..49273c4146 100644 --- a/interp/syntax_def.ml +++ b/interp/syntax_def.ml @@ -105,3 +105,10 @@ let search_syntactic_definition ?loc kn = let def = out_pat pat in verbose_compat ?loc kn def v; def + +let search_filtered_syntactic_definition ?loc filter kn = + let pat,v = KNmap.find kn !syntax_table in + let def = out_pat pat in + let res = filter def in + (match res with Some _ -> verbose_compat ?loc kn def v | None -> ()); + res diff --git a/interp/syntax_def.mli b/interp/syntax_def.mli index c5b6655ff8..77873f8f67 100644 --- a/interp/syntax_def.mli +++ b/interp/syntax_def.mli @@ -19,3 +19,6 @@ val declare_syntactic_definition : bool -> Id.t -> Flags.compat_version option -> syndef_interpretation -> unit val search_syntactic_definition : ?loc:Loc.t -> KerName.t -> syndef_interpretation + +val search_filtered_syntactic_definition : ?loc:Loc.t -> + (syndef_interpretation -> 'a option) -> KerName.t -> 'a option diff --git a/test-suite/bugs/closed/bug_9166.v b/test-suite/bugs/closed/bug_9166.v new file mode 100644 index 0000000000..8a7e9c37b0 --- /dev/null +++ b/test-suite/bugs/closed/bug_9166.v @@ -0,0 +1,9 @@ +Set Warnings "+deprecated". + +Notation bar := option (compat "8.7"). + +Definition foo (x: nat) : nat := + match x with + | 0 => 0 + | S bar => bar + end. |