diff options
| author | Jason Gross | 2017-06-01 18:21:29 -0400 |
|---|---|---|
| committer | Jason Gross | 2018-08-31 20:05:53 -0400 |
| commit | 35916e2a3a9ccae1ece8ce64ddf55faa50ac88b6 (patch) | |
| tree | 4ad0285d77c5c5a0f4188084dde9f88739a4f810 /plugins/syntax | |
| parent | 0ad2b76facd787f4b9b6f604f45199e549fe8f9c (diff) | |
Error on polymorphic conversions for numeral notations
Diffstat (limited to 'plugins/syntax')
| -rw-r--r-- | plugins/syntax/g_numeral.ml4 | 10 |
1 files changed, 8 insertions, 2 deletions
diff --git a/plugins/syntax/g_numeral.ml4 b/plugins/syntax/g_numeral.ml4 index 78461fe87d..9edb7c3351 100644 --- a/plugins/syntax/g_numeral.ml4 +++ b/plugins/syntax/g_numeral.ml4 @@ -405,7 +405,10 @@ let vernac_numeral_notation ty f g scope opts = in (* Check the type of f *) let to_kind = - if has_type f (arrow cint cty) then Int, Direct + if Global.is_polymorphic (Nametab.global f) then + CErrors.user_err + (pr_reference f ++ str " cannot be polymorphic for the moment") + else if has_type f (arrow cint cty) then Int, Direct else if has_type f (arrow cint (opt cty)) then Int, Option else if has_type f (arrow cuint cty) then UInt, Direct else if has_type f (arrow cuint (opt cty)) then UInt, Option @@ -425,7 +428,10 @@ let vernac_numeral_notation ty f g scope opts = in (* Check the type of g *) let of_kind = - if has_type g (arrow cty cint) then Int, Direct + if Global.is_polymorphic (Nametab.global g) then + CErrors.user_err + (pr_reference g ++ str " cannot be polymorphic for the moment") + else if has_type g (arrow cty cint) then Int, Direct else if has_type g (arrow cty (opt cint)) then Int, Option else if has_type g (arrow cty cuint) then UInt, Direct else if has_type g (arrow cty (opt cuint)) then UInt, Option |