diff options
| -rw-r--r-- | contrib/xml/xmlcommand.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/contrib/xml/xmlcommand.ml b/contrib/xml/xmlcommand.ml index 8e3d7cc35b..b071a65130 100644 --- a/contrib/xml/xmlcommand.ml +++ b/contrib/xml/xmlcommand.ml @@ -442,7 +442,7 @@ let kind_of_theorem = function | Decl_kinds.Remark -> "Remark" let kind_of_global_goal = function - | Decl_kinds.IsGlobal Decl_kinds.DefinitionBody -> "DEFINITION","Definition" + | Decl_kinds.IsGlobal Decl_kinds.DefinitionBody -> "DEFINITION","InteractiveDefinition" | Decl_kinds.IsGlobal (Decl_kinds.Proof k) -> "THEOREM",kind_of_theorem k | Decl_kinds.IsLocal -> assert false |