diff options
| author |  Stephane Glondu <steph@glondu.net> | 2014-01-19 15:09:23 +0100 |
|---|---|---|
| committer | Stephane Glondu <steph@glondu.net> | 2014-01-19 15:09:23 +0100 |
| commit | d2c5c5e616a6e118291fe1ce9965c731adac03a8 (patch) | |
| tree | 7b000ad50dcc45ff1c63768a983cded1e23a07ca /plugins/xml | |
| parent | db38bb4ad9aff74576d3b7f00028d48f0447d5bd (diff) | |
Imported Upstream version 8.4pl3dfsgupstream/8.4pl3dfsg
Diffstat (limited to 'plugins/xml')
| -rw-r--r-- | plugins/xml/cic2acic.ml | 2 | ||||
| -rw-r--r-- | plugins/xml/xmlcommand.ml | 26 |
2 files changed, 14 insertions, 14 deletions
diff --git a/plugins/xml/cic2acic.ml b/plugins/xml/cic2acic.ml index a14eda60..165bf83d 100644 --- a/plugins/xml/cic2acic.ml +++ b/plugins/xml/cic2acic.ml @@ -23,7 +23,7 @@ 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 "^ + Pp.msg_warn ("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 867aac71..59ade01e 100644 --- a/plugins/xml/xmlcommand.ml +++ b/plugins/xml/xmlcommand.ml @@ -433,46 +433,46 @@ let kind_of_constant kn = | DK.IsAssumption DK.Definitional -> "AXIOM","Declaration" | DK.IsAssumption DK.Logical -> "AXIOM","Axiom" | DK.IsAssumption DK.Conjectural -> - Pp.warning "Conjecture not supported in dtd (used Declaration instead)"; + Pp.msg_warn "Conjecture not supported in dtd (used Declaration instead)"; "AXIOM","Declaration" | DK.IsDefinition DK.Definition -> "DEFINITION","Definition" | DK.IsDefinition DK.Example -> - Pp.warning "Example not supported in dtd (used Definition instead)"; + Pp.msg_warn "Example not supported in dtd (used Definition instead)"; "DEFINITION","Definition" | DK.IsDefinition DK.Coercion -> - Pp.warning "Coercion not supported in dtd (used Definition instead)"; + Pp.msg_warn "Coercion not supported in dtd (used Definition instead)"; "DEFINITION","Definition" | DK.IsDefinition DK.SubClass -> - Pp.warning "SubClass not supported in dtd (used Definition instead)"; + Pp.msg_warn "SubClass not supported in dtd (used Definition instead)"; "DEFINITION","Definition" | DK.IsDefinition DK.CanonicalStructure -> - Pp.warning "CanonicalStructure not supported in dtd (used Definition instead)"; + Pp.msg_warn "CanonicalStructure not supported in dtd (used Definition instead)"; "DEFINITION","Definition" | DK.IsDefinition DK.Fixpoint -> - Pp.warning "Fixpoint not supported in dtd (used Definition instead)"; + Pp.msg_warn "Fixpoint not supported in dtd (used Definition instead)"; "DEFINITION","Definition" | DK.IsDefinition DK.CoFixpoint -> - Pp.warning "CoFixpoint not supported in dtd (used Definition instead)"; + Pp.msg_warn "CoFixpoint not supported in dtd (used Definition instead)"; "DEFINITION","Definition" | DK.IsDefinition DK.Scheme -> - Pp.warning "Scheme not supported in dtd (used Definition instead)"; + Pp.msg_warn "Scheme not supported in dtd (used Definition instead)"; "DEFINITION","Definition" | DK.IsDefinition DK.StructureComponent -> - Pp.warning "StructureComponent not supported in dtd (used Definition instead)"; + Pp.msg_warn "StructureComponent not supported in dtd (used Definition instead)"; "DEFINITION","Definition" | DK.IsDefinition DK.IdentityCoercion -> - Pp.warning "IdentityCoercion not supported in dtd (used Definition instead)"; + Pp.msg_warn "IdentityCoercion not supported in dtd (used Definition instead)"; "DEFINITION","Definition" | DK.IsDefinition DK.Instance -> - Pp.warning "Instance not supported in dtd (used Definition instead)"; + Pp.msg_warn "Instance not supported in dtd (used Definition instead)"; "DEFINITION","Definition" | DK.IsDefinition DK.Method -> - Pp.warning "Method not supported in dtd (used Definition instead)"; + Pp.msg_warn "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)"; + Pp.msg_warn "Unsupported theorem kind (used Theorem instead)"; "THEOREM",DK.string_of_theorem_kind DK.Theorem ;; |