diff options
| author |  Matej Kosik <m4tej.kosik@gmail.com> | 2015-12-16 14:27:20 +0100 |
|---|---|---|
| committer | Matej Kosik <m4tej.kosik@gmail.com> | 2015-12-18 15:57:55 +0100 |
| commit | ee3d0f32051d98bdba2a4ad2234966a2fa30a8ec (patch) | |
| tree | 6577dfe31111cf3c3d2e8166780aeb645950b9cf | |
| parent | 5174ee7e118d2bc57fc2d8a6619101735af79b16 (diff) | |
ALPHA-CONVERSION: in "parsing/g_vernac.ml4" file
| -rw-r--r-- | parsing/g_vernac.ml4 | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index 975dee934..2c9894dad 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -174,13 +174,13 @@ GEXTEND Gram ; END -let test_plurial_form = function +let test_plural_form = function | [(_,([_],_))] -> Flags.if_verbose msg_warning (strbrk "Keywords Variables/Hypotheses/Parameters expect more than one assumption") | _ -> () -let test_plurial_form_types = function +let test_plural_form_types = function | [([_],_)] -> Flags.if_verbose msg_warning (strbrk "Keywords Implicit Types expect more than one type") @@ -201,7 +201,7 @@ GEXTEND Gram | stre = assumption_token; nl = inline; bl = assum_list -> VernacAssumption (stre, nl, bl) | stre = assumptions_token; nl = inline; bl = assum_list -> - test_plurial_form bl; + test_plural_form bl; VernacAssumption (stre, nl, bl) | d = def_token; id = pidentref; b = def_body -> VernacDefinition (d, id, b) @@ -733,7 +733,7 @@ GEXTEND Gram VernacReserve bl | IDENT "Implicit"; IDENT "Types"; bl = reserv_list -> - test_plurial_form_types bl; + test_plural_form_types bl; VernacReserve bl | IDENT "Generalizable"; |