From f2b9dfdfb72abb3b797bd651a5846a7e7c761847 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Thu, 21 Jun 2007 17:01:21 +0000
Subject: Correction de plusieurs bugs de l'export XML (utilisation d'un type
 de constante par defaut pour les nouveaux types plutot qu'echouer;
 avertissement plutot qu'echec en cas de foncteur; nommage systematique des
 LetIn -- p.ex. functional induction engendre des LetIn non nommes --;
 branchement de la fonction de normalisation de tete evitant CProp sur Closure
 au lieu de Tacred afin de garantir la f.n. de tete)

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

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

diff --git a/contrib/xml/xmlcommand.ml b/contrib/xml/xmlcommand.ml
index f286d2c8a5..0127132399 100644
--- a/contrib/xml/xmlcommand.ml
+++ b/contrib/xml/xmlcommand.ml
@@ -461,11 +461,42 @@ let kind_of_constant kn =
   match Declare.constant_kind (Nametab.sp_of_global(Libnames.ConstRef kn)) with
     | DK.IsAssumption DK.Definitional -> "AXIOM","Declaration"
     | DK.IsAssumption DK.Logical -> "AXIOM","Axiom"
-    | DK.IsAssumption DK.Conjectural -> "AXIOM","Conjecture"
+    | DK.IsAssumption DK.Conjectural ->
+        Pp.warning "Conjecture not supported in dtd (used Declaration instead)";
+        "AXIOM","Declaration"
     | DK.IsDefinition DK.Definition -> "DEFINITION","Definition"
-    | DK.IsDefinition DK.Example -> "DEFINITION","Example"
-    | DK.IsDefinition _ -> Util.anomaly "Unsupported constant kind"
-    | DK.IsProof thm -> "THEOREM",DK.string_of_theorem_kind thm
+    | DK.IsDefinition DK.Example -> 
+        Pp.warning "Example not supported in dtd (used Definition instead)";
+        "DEFINITION","Definition"
+    | DK.IsDefinition DK.Coercion ->
+        Pp.warning "Coercion not supported in dtd (used Definition instead)";
+        "DEFINITION","Definition"
+    | DK.IsDefinition DK.SubClass ->
+        Pp.warning "SubClass not supported in dtd (used Definition instead)";
+        "DEFINITION","Definition"
+    | DK.IsDefinition DK.CanonicalStructure ->
+        Pp.warning "CanonicalStructure not supported in dtd (used Definition instead)";
+        "DEFINITION","Definition"
+    | DK.IsDefinition DK.Fixpoint ->
+        Pp.warning "Fixpoint not supported in dtd (used Definition instead)";
+        "DEFINITION","Definition"
+    | DK.IsDefinition DK.CoFixpoint ->
+        Pp.warning "CoFixpoint not supported in dtd (used Definition instead)";
+        "DEFINITION","Definition"
+    | DK.IsDefinition DK.Scheme ->
+        Pp.warning "Scheme not supported in dtd (used Definition instead)";
+        "DEFINITION","Definition"
+    | DK.IsDefinition DK.StructureComponent ->
+        Pp.warning "StructureComponent not supported in dtd (used Definition instead)";
+        "DEFINITION","Definition"
+    | 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) ->
+        "THEOREM",DK.string_of_theorem_kind thm
+    | DK.IsProof _ ->
+        Pp.warning "Unsupported theorem kind (used Theorem instead)";
+        "THEOREM",DK.string_of_theorem_kind DK.Theorem
 ;;
 
 let kind_of_global r =
-- 
cgit v1.2.3