diff options
| author | Matthieu Sozeau | 2014-07-24 17:47:40 +0200 |
|---|---|---|
| committer | Matthieu Sozeau | 2014-07-24 17:47:40 +0200 |
| commit | 31c1280a000c03c3a48ee697032d67e3e06af3fa (patch) | |
| tree | 18a66206265e37b1312966ca25aa7f5ebc3c00da | |
| parent | ae5ea0c9d5c0e9a39a50a2348b2b8f08938d5f5c (diff) | |
Fix misleading pretty-printing of information for non-universe-polymorphic
definitions.
| -rw-r--r-- | printing/prettyp.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/printing/prettyp.ml b/printing/prettyp.ml index 03ad7889fa..42d779f04d 100644 --- a/printing/prettyp.ml +++ b/printing/prettyp.ml @@ -202,7 +202,7 @@ let print_polymorphism ref = (if poly then "universe polymorphic" else if template_poly then "template universe polymorphic" - else "monomorphic") + else "not universe polymorphic") let print_name_infos ref = let poly = print_polymorphism ref in |