diff options
| author | Hugo Herbelin | 2016-03-13 13:18:10 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2016-03-13 13:18:54 +0100 |
| commit | d868820ad1f00b896c5f44f18678fac2f8e0f720 (patch) | |
| tree | 2312a62d9fd275d1c70b5e4fabcbe308826d5a05 /plugins | |
| parent | 7478ad7cc600753ba2609254657c87cacc27e8fc (diff) | |
Supporting "(@foo) args" in patterns, where "@foo" has no arguments.
Diffstat (limited to 'plugins')
| -rw-r--r-- | plugins/decl_mode/decl_interp.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/decl_mode/decl_interp.ml b/plugins/decl_mode/decl_interp.ml index 4874552d6a..34307a358f 100644 --- a/plugins/decl_mode/decl_interp.ml +++ b/plugins/decl_mode/decl_interp.ml @@ -96,7 +96,7 @@ let rec add_vars_of_simple_pattern globs = function add_vars_of_simple_pattern globs p | CPatCstr (_,_,pl1,pl2) -> List.fold_left add_vars_of_simple_pattern - (List.fold_left add_vars_of_simple_pattern globs pl1) pl2 + (Option.fold_left (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 |