diff options
Diffstat (limited to 'interp/topconstr.ml')
| -rw-r--r-- | interp/topconstr.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/interp/topconstr.ml b/interp/topconstr.ml index c8fbdaf28..2ffeb1f83 100644 --- a/interp/topconstr.ml +++ b/interp/topconstr.ml @@ -282,7 +282,7 @@ let locs_of_notation loc locs ntn = let ntn_loc loc (args,argslist,binderslist) = locs_of_notation loc (List.map constr_loc (args@List.flatten argslist)@ - List.map local_binders_loc binderslist) + List.map_filter local_binders_loc binderslist) let patntn_loc loc (args,argslist) = locs_of_notation loc |