diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-03-19 17:24:25 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-03-19 17:24:25 +0000 |
| commit | e5320fdb6a60b6593458ea123a74f5cc31cf8df4 (patch) | |
| tree | 7c29b832a3d9a124067b005ae0a4c010c1d38c4e | |
| parent | 0158f832f5988fc91ed22e407645b657d7993b70 (diff) | |
Hopefully complying with camlp5 < 6.00 syntax
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15055 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | parsing/argextend.ml4 | 2 | ||||
| -rw-r--r-- | parsing/tacextend.ml4 | 2 |
2 files changed, 2 insertions, 2 deletions
diff --git a/parsing/argextend.ml4 b/parsing/argextend.ml4 index d890be142..e8d72740f 100644 --- a/parsing/argextend.ml4 +++ b/parsing/argextend.ml4 @@ -154,7 +154,7 @@ let possibly_empty_subentries loc (prods,act) = | _ -> assert false (* already filtered out *) in if has_extraarg prods then (* Needs a dynamic check *) - (true, <:expr< try Some $aux prods$ with Exit -> None >>) + (true, <:expr< try Some $aux prods$ with [ Exit -> None ] >>) else (* Static optimisation *) (false, aux prods) diff --git a/parsing/tacextend.ml4 b/parsing/tacextend.ml4 index 73ef0d701..95f916f55 100644 --- a/parsing/tacextend.ml4 +++ b/parsing/tacextend.ml4 @@ -141,7 +141,7 @@ let rec possibly_empty_subentries loc = function raise Exit) prods in if has_extraarg prods then (true,<:expr< try Some $mlexpr_of_list (fun x -> x) l$ - with Failure "" -> $snd (aux rest)$ >>) + with [ Failure "" -> $snd (aux rest)$ ] >>) else (true, <:expr< Some $mlexpr_of_list (fun x -> x) l$ >>) with Exit -> aux rest in |