aboutsummaryrefslogtreecommitdiffhomepage
path: root/library/kindops.ml
diff options
context:
space:
mode:
authorGravatar ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7>2013-01-28 21:05:35 +0000
committerGravatar ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7>2013-01-28 21:05:35 +0000
commit5a39e6c08d428d774165e0ef3922ba8b75eee9e1 (patch)
treee035f490e2c748356df73342876b22cfcb3bc5a0 /library/kindops.ml
parent5e8824960f68f529869ac299b030282cc916ba2c (diff)
Uniformization of the "anomaly" command.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16165 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'library/kindops.ml')
-rw-r--r--library/kindops.ml4
1 files changed, 2 insertions, 2 deletions
diff --git a/library/kindops.ml b/library/kindops.ml
index 86e6e2fff..35aebc531 100644
--- a/library/kindops.ml
+++ b/library/kindops.ml
@@ -34,8 +34,8 @@ let string_of_definition_kind def =
| Global, CanonicalStructure -> "Canonical Structure"
| Global, Example -> "Example"
| Local, (CanonicalStructure|Example) ->
- Errors.anomaly "Unsupported local definition kind"
+ Errors.anomaly (Pp.str "Unsupported local definition kind")
| Local, Instance -> "Instance"
| Global, Instance -> "Global Instance"
| _, (StructureComponent|Scheme|CoFixpoint|Fixpoint|IdentityCoercion|Method)
- -> Errors.anomaly "Internal definition kind"
+ -> Errors.anomaly (Pp.str "Internal definition kind")