diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2016-04-26 06:06:17 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2016-04-27 21:55:49 +0200 |
| commit | 857dc0aaae30805725da213b6550dc1ff3a7adb2 (patch) | |
| tree | 2f083695ad7d49fff21a572fd4969a06d01fedcc /parsing | |
| parent | 239f30c2070018db88e568acca6c9054f650ca38 (diff) | |
Fixing a mispelling coma -> comma.
Diffstat (limited to 'parsing')
| -rw-r--r-- | parsing/g_tactic.ml4 | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4 index d36399c0d..506bb1d53 100644 --- a/parsing/g_tactic.ml4 +++ b/parsing/g_tactic.ml4 @@ -111,8 +111,8 @@ let check_for_coloneq = | KEYWORD "(" -> skip_binders 2 | _ -> err ()) -let lookup_at_as_coma = - Gram.Entry.of_parser "lookup_at_as_coma" +let lookup_at_as_comma = + Gram.Entry.of_parser "lookup_at_as_comma" (fun strm -> match get_tok (stream_nth 0 strm) with | KEYWORD (","|"at"|"as") -> () @@ -595,7 +595,7 @@ GEXTEND Gram | IDENT "generalize"; c = constr; l = LIST1 constr -> let gen_everywhere c = ((AllOccurrences,c),Names.Anonymous) in TacAtom (!@loc, TacGeneralize (List.map gen_everywhere (c::l))) - | IDENT "generalize"; c = constr; lookup_at_as_coma; nl = occs; + | IDENT "generalize"; c = constr; lookup_at_as_comma; nl = occs; na = as_name; l = LIST0 [","; c = pattern_occ; na = as_name -> (c,na)] -> TacAtom (!@loc, TacGeneralize (((nl,c),na)::l)) |