diff options
| author | herbelin | 2007-06-21 17:01:21 +0000 |
|---|---|---|
| committer | herbelin | 2007-06-21 17:01:21 +0000 |
| commit | f2b9dfdfb72abb3b797bd651a5846a7e7c761847 (patch) | |
| tree | 6a42b2ede058ded7671cc6fc17db1698ec3ca2fa /contrib/xml/xmlcommand.ml | |
| parent | bd5b2a45c2ef00d63fc84f5f1bc577fcb3a3d0d9 (diff) | |
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
Diffstat (limited to 'contrib/xml/xmlcommand.ml')
| -rw-r--r-- | contrib/xml/xmlcommand.ml | 39 |
1 files changed, 35 insertions, 4 deletions
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 = |