diff options
| -rw-r--r-- | toplevel/class.ml | 5 |
1 files changed, 0 insertions, 5 deletions
diff --git a/toplevel/class.ml b/toplevel/class.ml index 57afbb5e55..667e127061 100644 --- a/toplevel/class.ml +++ b/toplevel/class.ml @@ -296,11 +296,6 @@ let get_strength stre ref cls clt = *) let streunif = NeverDischarge in let stre' = stre_max4 stres stret stref streunif in - if (stre = NeverDischarge) & (stre' <> NeverDischarge) - then errorlabstrm "try_add_coercion" - [< Printer.pr_global ref; - 'sTR " must be declared as a local coercion"; 'fNL; - 'sTR "because it involves local definition" >]; stre_max (stre,stre') (* coercion identité *) |