diff options
| author | Maxime Dénès | 2017-03-22 14:09:41 +0100 |
|---|---|---|
| committer | Maxime Dénès | 2017-03-22 14:09:41 +0100 |
| commit | 6e0ca299c407125a8d65f54ab424bdae3667125e (patch) | |
| tree | 2f968c31b85b22190d4ce9f2472f4cb6cd0a6ad9 /engine | |
| parent | 051ef20a9f9c496fc6a5143de97450ccf7786c5b (diff) | |
| parent | aa9e94275ccac92311a6bdac563b61a6c7876cec (diff) | |
Merge PR#390: Updates to the Pretty Printing Infrastructure
Diffstat (limited to 'engine')
| -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 6720fcef8f..30a9ef1634 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 |