diff options
-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 |