diff options
author | 2016-04-27 22:13:02 +0200 | |
---|---|---|
committer | 2016-04-27 22:13:02 +0200 | |
commit | 19ab3add0560dbc6c42e012c61964ba89b399429 (patch) | |
tree | b04784f0b8f7c9f424361c1783b3a7a9f48d83d3 /parsing | |
parent | 2f772c3347c45cb5173472924a69ab83dd9da626 (diff) |
Revert "Fixing a mispelling coma -> comma."
This reverts commit 857dc0aaae30805725da213b6550dc1ff3a7adb2.
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 506bb1d53..d36399c0d 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_comma = - Gram.Entry.of_parser "lookup_at_as_comma" +let lookup_at_as_coma = + Gram.Entry.of_parser "lookup_at_as_coma" (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_comma; nl = occs; + | IDENT "generalize"; c = constr; lookup_at_as_coma; nl = occs; na = as_name; l = LIST0 [","; c = pattern_occ; na = as_name -> (c,na)] -> TacAtom (!@loc, TacGeneralize (((nl,c),na)::l)) |