diff options
author | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2016-04-26 06:06:17 +0200 |
---|---|---|
committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2016-06-16 17:43:29 +0200 |
commit | 69ed6089d7ed778e37f5442f57ef7693f73ca802 (patch) | |
tree | c3a9e94cba91212b1110ec62bb0c5ca045821c08 | |
parent | bf3ef955995c39049d9a7f68797a6c3f045a2464 (diff) |
Fixing a mispelling coma -> comma.
-rw-r--r-- | parsing/g_tactic.ml4 | 6 | ||||
-rw-r--r-- | plugins/funind/g_indfun.ml4 | 10 |
2 files changed, 8 insertions, 8 deletions
diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4 index f2e1f904b..024b51941 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)) diff --git a/plugins/funind/g_indfun.ml4 b/plugins/funind/g_indfun.ml4 index aa9cc4023..893baad8c 100644 --- a/plugins/funind/g_indfun.ml4 +++ b/plugins/funind/g_indfun.ml4 @@ -123,12 +123,12 @@ TACTIC EXTEND snewfunind END -let pr_constr_coma_sequence prc _ _ = prlist_with_sep pr_comma prc +let pr_constr_comma_sequence prc _ _ = prlist_with_sep pr_comma prc -ARGUMENT EXTEND constr_coma_sequence' +ARGUMENT EXTEND constr_comma_sequence' TYPED AS constr_list - PRINTED BY pr_constr_coma_sequence -| [ constr(c) "," constr_coma_sequence'(l) ] -> [ c::l ] + PRINTED BY pr_constr_comma_sequence +| [ constr(c) "," constr_comma_sequence'(l) ] -> [ c::l ] | [ constr(c) ] -> [ [c] ] END @@ -137,7 +137,7 @@ let pr_auto_using prc _prlc _prt = Pptactic.pr_auto_using prc ARGUMENT EXTEND auto_using' TYPED AS constr_list PRINTED BY pr_auto_using -| [ "using" constr_coma_sequence'(l) ] -> [ l ] +| [ "using" constr_comma_sequence'(l) ] -> [ l ] | [ ] -> [ [] ] END |