diff options
| author | ppedrot | 2013-10-09 20:31:01 +0000 |
|---|---|---|
| committer | ppedrot | 2013-10-09 20:31:01 +0000 |
| commit | 26d5b958417be3750bd767ede0128510fe8508b8 (patch) | |
| tree | 9355965a5e37713e2eef951ae6d5fffb4f2227b1 | |
| parent | fc4a50be24c2026947253c4f0820c9d714f51a75 (diff) | |
Fixing CAMLP4 compilation.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16865 85f007b7-540e-0410-9357-904b9bb8a0f7
| -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 |