diff options
Diffstat (limited to 'plugins/decl_mode')
| -rw-r--r-- | plugins/decl_mode/decl_interp.ml | 9 |
1 files changed, 5 insertions, 4 deletions
diff --git a/plugins/decl_mode/decl_interp.ml b/plugins/decl_mode/decl_interp.ml index 6d3a5be392..a067440cbb 100644 --- a/plugins/decl_mode/decl_interp.ml +++ b/plugins/decl_mode/decl_interp.ml @@ -96,10 +96,11 @@ let rec add_vars_of_simple_pattern globs = function (UserError ("simple_pattern",str "\"(_ | _)\" is not allowed here")) | CPatDelimiters (_,_,p) -> add_vars_of_simple_pattern globs p - | CPatCstr (_,_,pl) | CPatCstrExpl (_,_,pl) -> - List.fold_left add_vars_of_simple_pattern globs pl - | CPatNotation(_,_,(pl,pll)) -> - List.fold_left add_vars_of_simple_pattern globs (List.flatten (pl::pll)) + | CPatCstr (_,_,pl1,pl2) -> + List.fold_left add_vars_of_simple_pattern + (List.fold_left add_vars_of_simple_pattern globs pl1) pl2 + | CPatNotation(_,_,(pl,pll),pl') -> + List.fold_left add_vars_of_simple_pattern globs (List.flatten (pl::pl'::pll)) | CPatAtom (_,Some (Libnames.Ident (_,id))) -> add_var id globs | _ -> globs |