diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2016-04-27 22:13:02 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2016-04-27 22:13:02 +0200 |
| commit | 19ab3add0560dbc6c42e012c61964ba89b399429 (patch) | |
| tree | b04784f0b8f7c9f424361c1783b3a7a9f48d83d3 /plugins/funind/g_indfun.ml4 | |
| parent | 2f772c3347c45cb5173472924a69ab83dd9da626 (diff) | |
Revert "Fixing a mispelling coma -> comma."
This reverts commit 857dc0aaae30805725da213b6550dc1ff3a7adb2.
Diffstat (limited to 'plugins/funind/g_indfun.ml4')
| -rw-r--r-- | plugins/funind/g_indfun.ml4 | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/plugins/funind/g_indfun.ml4 b/plugins/funind/g_indfun.ml4 index a9617a6c5..0760e78bf 100644 --- a/plugins/funind/g_indfun.ml4 +++ b/plugins/funind/g_indfun.ml4 @@ -125,12 +125,12 @@ TACTIC EXTEND snewfunind END -let pr_constr_comma_sequence prc _ _ = prlist_with_sep pr_comma prc +let pr_constr_coma_sequence prc _ _ = prlist_with_sep pr_comma prc -ARGUMENT EXTEND constr_comma_sequence' +ARGUMENT EXTEND constr_coma_sequence' TYPED AS constr_list - PRINTED BY pr_constr_comma_sequence -| [ constr(c) "," constr_comma_sequence'(l) ] -> [ c::l ] + PRINTED BY pr_constr_coma_sequence +| [ constr(c) "," constr_coma_sequence'(l) ] -> [ c::l ] | [ constr(c) ] -> [ [c] ] END @@ -139,7 +139,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_comma_sequence'(l) ] -> [ l ] +| [ "using" constr_coma_sequence'(l) ] -> [ l ] | [ ] -> [ [] ] END |