From f350cd8cb53e675a5793336b9b17c4749fa474b8 Mon Sep 17 00:00:00 2001
From: msozeau
Date: Fri, 30 May 2008 12:41:39 +0000
Subject: Improvements on coqdoc by adding more information into .glob files,
 about definitions and type of references. - Add missing location information
 on fixpoints/cofixpoint in topconstr and syntactic definitions in
 vernacentries for correct dumping. - Dump definition information in
 vernacentries: defs, constructors, projections etc... - Modify
 coqdoc/index.mll to use this information instead of trying to scan the file.
 - Use the type information in latex output, update coqdoc.sty accordingly. -
 Use the hyperref package to do crossrefs between definition and   references
 to coq objects in latex.

Next step is to test and debug it on bigger developments.

On the side:
- Fix Program Let which was adding a Global definition. 
- Correct implicits for well-founded Program Fixpoints.
- Add new [Method] declaration kind.


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

(limited to 'contrib/xml')

diff --git a/contrib/xml/xmlcommand.ml b/contrib/xml/xmlcommand.ml
index 7e3a1bd410..3c4b01f5bb 100644
--- a/contrib/xml/xmlcommand.ml
+++ b/contrib/xml/xmlcommand.ml
@@ -487,7 +487,10 @@ let kind_of_constant kn =
     | 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) ->
+    | DK.IsDefinition DK.Method ->
+        Pp.warning "Method 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)";
-- 
cgit v1.2.3