diff options
Diffstat (limited to 'parsing/g_tactic.ml4')
| -rw-r--r-- | parsing/g_tactic.ml4 | 11 |
1 files changed, 6 insertions, 5 deletions
diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4 index 7bebf6db..ad093507 100644 --- a/parsing/g_tactic.ml4 +++ b/parsing/g_tactic.ml4 @@ -8,7 +8,7 @@ (*i camlp4use: "pa_extend.cmo" i*) -(* $Id: g_tactic.ml4 11741 2009-01-03 14:34:39Z herbelin $ *) +(* $Id: g_tactic.ml4 12009 2009-03-23 22:55:37Z herbelin $ *) open Pp open Pcoq @@ -72,15 +72,16 @@ let test_lpar_id_colon = let check_for_coloneq = Gram.Entry.of_parser "lpar_id_colon" (fun strm -> - let rec skip_to_rpar n = + let rec skip_to_rpar p n = match list_last (Stream.npeek n strm) with - | ("",")") -> n+1 + | ("","(") -> skip_to_rpar (p+1) (n+1) + | ("",")") -> if p=0 then n+1 else skip_to_rpar (p-1) (n+1) | ("",".") -> raise Stream.Failure - | _ -> skip_to_rpar (n+1) in + | _ -> skip_to_rpar p (n+1) in let rec skip_names n = match list_last (Stream.npeek n strm) with | ("IDENT",_) | ("","_") -> skip_names (n+1) - | ("",":") -> skip_to_rpar (n+1) (* skip a constr *) + | ("",":") -> skip_to_rpar 0 (n+1) (* skip a constr *) | _ -> raise Stream.Failure in let rec skip_binders n = match list_last (Stream.npeek n strm) with |