diff options
| author | Pierre-Marie Pédrot | 2018-12-13 13:44:31 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2018-12-13 13:44:31 +0100 |
| commit | caa4a00c4d428325484a8701fbf585e8d522acdf (patch) | |
| tree | fe30358f63202fa405cce5fcd9f8b2858adcab2b /interp | |
| parent | cb2de56d13a67d5e3a2fa3358fd1b35e14bfbd54 (diff) | |
| parent | 412a96a5c3560fee1adad87a3ba1aa1d324ab039 (diff) | |
Merge PR #9167: Fixes #9166: no deprecation warning on aliases used as pattern variables
Diffstat (limited to 'interp')
| -rw-r--r-- | interp/constrintern.ml | 8 | ||||
| -rw-r--r-- | interp/syntax_def.ml | 7 | ||||
| -rw-r--r-- | interp/syntax_def.mli | 3 |
3 files changed, 15 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 |