diff options
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 |