diff options
Diffstat (limited to 'grammar/vernacextend.ml4')
| -rw-r--r-- | grammar/vernacextend.ml4 | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/grammar/vernacextend.ml4 b/grammar/vernacextend.ml4 index 0d91c796ad..ad8929657a 100644 --- a/grammar/vernacextend.ml4 +++ b/grammar/vernacextend.ml4 @@ -44,8 +44,9 @@ let mk_ignore c pt = let names = CList.map_filter (function | GramNonTerminal(_,_,_,Some p) -> Some (Names.Id.to_string p) | _ -> None) pt in - let names = List.map (fun n -> <:expr< $lid:n$ >>) names in - <:expr< do { ignore($list:names$); $c$ } >> + let fold accu id = <:expr< let _ = $lid:id$ in $accu$ >> in + let names = List.fold_left fold <:expr< () >> names in + <:expr< do { let _ = $names$ in $c$ } >> let make_clause_classifier cg s (_,pt,c,_) = match c ,cg with |