diff options
Diffstat (limited to 'contrib/xml/xmlcommand.ml')
| -rw-r--r-- | contrib/xml/xmlcommand.ml | 5 |
1 files changed, 4 insertions, 1 deletions
diff --git a/contrib/xml/xmlcommand.ml b/contrib/xml/xmlcommand.ml index 82d7c19e51..3a0fdfb9b9 100644 --- a/contrib/xml/xmlcommand.ml +++ b/contrib/xml/xmlcommand.ml @@ -491,7 +491,10 @@ let kind_of_constant kn = | DK.IsDefinition DK.IdentityCoercion -> Pp.warning "IdentityCoercion not supported in dtd (used Definition instead)"; "DEFINITION","Definition" - | DK.IsProof (DK.Theorem|DK.Lemma|DK.Corollary|DK.Fact|DK.Remark as thm) -> + | DK.IsDefinition DK.Instance -> + Pp.warning "Instance not supported in dtd (used Definition instead)"; + "DEFINITION","Definition" + | DK.IsProof (DK.Theorem|DK.Lemma|DK.Corollary|DK.Fact|DK.Remark as thm) -> "THEOREM",DK.string_of_theorem_kind thm | DK.IsProof _ -> Pp.warning "Unsupported theorem kind (used Theorem instead)"; |