From 2bb215ff6f65713312bfa207c3937628bd0b02f8 Mon Sep 17 00:00:00 2001
From: sacerdot
Date: Sun, 4 Apr 2004 13:42:54 +0000
Subject: ** WARNING ** DTD Change.

ht:DEFINITION/Definition differentiated into
 ht:DEFINITION/Definition and
 ht:DEFINITION/InteractiveDefinition

because of an explicit request of Iris Loeb.

HELM/MoWGLI DTD and Stylesheet changed accordingly.


git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5634 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 contrib/xml/xmlcommand.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'contrib/xml/xmlcommand.ml')

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
 
-- 
cgit v1.2.3