diff options
| author | Hugo Herbelin | 2016-04-26 06:06:17 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2016-06-16 17:43:29 +0200 |
| commit | 69ed6089d7ed778e37f5442f57ef7693f73ca802 (patch) | |
| tree | c3a9e94cba91212b1110ec62bb0c5ca045821c08 /parsing | |
| parent | bf3ef955995c39049d9a7f68797a6c3f045a2464 (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 f2e1f904b9..024b51941d 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") -> () @@ -585,7 +585,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)) |