diff options
| author |  Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-02-08 18:13:25 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-03-21 15:51:47 +0100 |
| commit | 921ea3983d45051ae85b0e20bf13de2eff38e53e (patch) | |
| tree | 6b8a7f33e7df5d2eac0c81a8839ca6d749fad752 /engine/universes.ml | |
| parent | 3b3d5937939ac8dc4f152d61391630e62bb0b2e5 (diff) | |
[pp] Remove uses of expensive string_of_ppcmds.
In general we want to avoid this as much as we can, as it will need to
make choices regarding the output backend (width, etc...) and it is
expensive. It is better to serve the printing backends the pretty
print document itself.
Diffstat (limited to 'engine/universes.ml')
| -rw-r--r-- | engine/universes.ml | 7 |
1 files changed, 3 insertions, 4 deletions
diff --git a/engine/universes.ml b/engine/universes.ml index 6720fcef8..30a9ef163 100644 --- a/engine/universes.ml +++ b/engine/universes.ml @@ -416,10 +416,9 @@ let constr_of_global gr = (* Should be an error as we might forget constraints, allow for now to make firstorder work with "using" clauses *) c - else raise (Invalid_argument - ("constr_of_global: globalization of polymorphic reference " ^ - Pp.string_of_ppcmds (Nametab.pr_global_env Id.Set.empty gr) ^ - " would forget universes.")) + else CErrors.user_err ~hdr:"constr_of_global" + Pp.(str "globalization of polymorphic reference " ++ Nametab.pr_global_env Id.Set.empty gr ++ + str " would forget universes.") else c let constr_of_reference = constr_of_global |