diff options
| author | Jason Gross | 2017-06-01 17:45:01 -0400 |
|---|---|---|
| committer | Jason Gross | 2018-08-31 20:05:53 -0400 |
| commit | 0ad2b76facd787f4b9b6f604f45199e549fe8f9c (patch) | |
| tree | daf8f4e9166e81030427a90951a45bb680472e77 /plugins | |
| parent | 1e49dad4c4ea721a0844d9553e84aed90777f46d (diff) | |
Fix grammar
```
git grep --name-only 'should goes' | xargs sed s'/should goes/should go/g' -i
```
Diffstat (limited to 'plugins')
| -rw-r--r-- | plugins/syntax/g_numeral.ml4 | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/plugins/syntax/g_numeral.ml4 b/plugins/syntax/g_numeral.ml4 index cb99904b6e..78461fe87d 100644 --- a/plugins/syntax/g_numeral.ml4 +++ b/plugins/syntax/g_numeral.ml4 @@ -411,7 +411,7 @@ let vernac_numeral_notation ty f g scope opts = else if has_type f (arrow cuint (opt cty)) then UInt, Option else if Option.is_empty z_pos_ty then CErrors.user_err - (pr_reference f ++ str " should goes from Decimal.int or uint to " ++ + (pr_reference f ++ str " should go from Decimal.int or uint to " ++ pr_reference ty ++ str " or (option " ++ pr_reference ty ++ str ")." ++ fnl () ++ str "Instead of int, the type Z could also be used (load it first).") @@ -419,7 +419,7 @@ let vernac_numeral_notation ty f g scope opts = else if has_type f (arrow cZ (opt cty)) then Z, Option else CErrors.user_err - (pr_reference f ++ str " should goes from Decimal.int or uint or Z to " + (pr_reference f ++ str " should go from Decimal.int or uint or Z to " ++ pr_reference ty ++ str " or (option " ++ pr_reference ty ++ str ")") in @@ -431,7 +431,7 @@ let vernac_numeral_notation ty f g scope opts = else if has_type g (arrow cty (opt cuint)) then UInt, Option else if Option.is_empty z_pos_ty then CErrors.user_err - (pr_reference g ++ str " should goes from " ++ + (pr_reference g ++ str " should go from " ++ pr_reference ty ++ str " to Decimal.int or (option int) or uint." ++ fnl () ++ str "Instead of int, the type Z could also be used (load it first).") @@ -439,7 +439,7 @@ let vernac_numeral_notation ty f g scope opts = else if has_type g (arrow cty (opt cZ)) then Z, Option else CErrors.user_err - (pr_reference g ++ str " should goes from " ++ + (pr_reference g ++ str " should go from " ++ pr_reference ty ++ str " to Decimal.int or (option int) or uint or Z or (option Z)") in |