From 24879dc0e59856e297b0172d00d67df67fbb0184 Mon Sep 17 00:00:00 2001 From: ppedrot Date: Wed, 30 May 2012 16:05:13 +0000 Subject: More uniformisation in Pp.warn functions. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15399 85f007b7-540e-0410-9357-904b9bb8a0f7 --- plugins/xml/cic2acic.ml | 4 ++-- plugins/xml/xmlcommand.ml | 26 +++++++++++++------------- 2 files changed, 15 insertions(+), 15 deletions(-) (limited to 'plugins/xml') diff --git a/plugins/xml/cic2acic.ml b/plugins/xml/cic2acic.ml index ec0910d7f..e29fcd0e8 100644 --- a/plugins/xml/cic2acic.ml +++ b/plugins/xml/cic2acic.ml @@ -23,8 +23,8 @@ let get_module_path_of_full_path path = (function modul -> Libnames.is_dirpath_prefix_of modul dirpath) modules with [] -> - Pp.warning ("Modules not supported: reference to "^ - Libnames.string_of_path path^" will be wrong"); + Pp.msg_warning (Pp.str ("Modules not supported: reference to "^ + Libnames.string_of_path path^" will be wrong")); dirpath | [modul] -> modul | _ -> diff --git a/plugins/xml/xmlcommand.ml b/plugins/xml/xmlcommand.ml index 81dba546e..ee9bcb25d 100644 --- a/plugins/xml/xmlcommand.ml +++ b/plugins/xml/xmlcommand.ml @@ -426,46 +426,46 @@ let kind_of_constant kn = | IsAssumption Definitional -> "AXIOM","Declaration" | IsAssumption Logical -> "AXIOM","Axiom" | IsAssumption Conjectural -> - Pp.warning "Conjecture not supported in dtd (used Declaration instead)"; + Pp.msg_warning (Pp.str "Conjecture not supported in dtd (used Declaration instead)"); "AXIOM","Declaration" | IsDefinition Definition -> "DEFINITION","Definition" | IsDefinition Example -> - Pp.warning "Example not supported in dtd (used Definition instead)"; + Pp.msg_warning (Pp.str "Example not supported in dtd (used Definition instead)"); "DEFINITION","Definition" | IsDefinition Coercion -> - Pp.warning "Coercion not supported in dtd (used Definition instead)"; + Pp.msg_warning (Pp.str "Coercion not supported in dtd (used Definition instead)"); "DEFINITION","Definition" | IsDefinition SubClass -> - Pp.warning "SubClass not supported in dtd (used Definition instead)"; + Pp.msg_warning (Pp.str "SubClass not supported in dtd (used Definition instead)"); "DEFINITION","Definition" | IsDefinition CanonicalStructure -> - Pp.warning "CanonicalStructure not supported in dtd (used Definition instead)"; + Pp.msg_warning (Pp.str "CanonicalStructure not supported in dtd (used Definition instead)"); "DEFINITION","Definition" | IsDefinition Fixpoint -> - Pp.warning "Fixpoint not supported in dtd (used Definition instead)"; + Pp.msg_warning (Pp.str "Fixpoint not supported in dtd (used Definition instead)"); "DEFINITION","Definition" | IsDefinition CoFixpoint -> - Pp.warning "CoFixpoint not supported in dtd (used Definition instead)"; + Pp.msg_warning (Pp.str "CoFixpoint not supported in dtd (used Definition instead)"); "DEFINITION","Definition" | IsDefinition Scheme -> - Pp.warning "Scheme not supported in dtd (used Definition instead)"; + Pp.msg_warning (Pp.str "Scheme not supported in dtd (used Definition instead)"); "DEFINITION","Definition" | IsDefinition StructureComponent -> - Pp.warning "StructureComponent not supported in dtd (used Definition instead)"; + Pp.msg_warning (Pp.str "StructureComponent not supported in dtd (used Definition instead)"); "DEFINITION","Definition" | IsDefinition IdentityCoercion -> - Pp.warning "IdentityCoercion not supported in dtd (used Definition instead)"; + Pp.msg_warning (Pp.str "IdentityCoercion not supported in dtd (used Definition instead)"); "DEFINITION","Definition" | IsDefinition Instance -> - Pp.warning "Instance not supported in dtd (used Definition instead)"; + Pp.msg_warning (Pp.str "Instance not supported in dtd (used Definition instead)"); "DEFINITION","Definition" | IsDefinition Method -> - Pp.warning "Method not supported in dtd (used Definition instead)"; + Pp.msg_warning (Pp.str "Method not supported in dtd (used Definition instead)"); "DEFINITION","Definition" | IsProof (Theorem|Lemma|Corollary|Fact|Remark as thm) -> "THEOREM",Kindops.string_of_theorem_kind thm | IsProof _ -> - Pp.warning "Unsupported theorem kind (used Theorem instead)"; + Pp.msg_warning (Pp.str "Unsupported theorem kind (used Theorem instead)"); "THEOREM",Kindops.string_of_theorem_kind Theorem ;; -- cgit v1.2.3