diff options
| author | ppedrot | 2013-01-28 21:05:35 +0000 |
|---|---|---|
| committer | ppedrot | 2013-01-28 21:05:35 +0000 |
| commit | 5a39e6c08d428d774165e0ef3922ba8b75eee9e1 (patch) | |
| tree | e035f490e2c748356df73342876b22cfcb3bc5a0 /plugins/xml/xmlcommand.ml | |
| parent | 5e8824960f68f529869ac299b030282cc916ba2c (diff) | |
Uniformization of the "anomaly" command.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16165 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'plugins/xml/xmlcommand.ml')
| -rw-r--r-- | plugins/xml/xmlcommand.ml | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/plugins/xml/xmlcommand.ml b/plugins/xml/xmlcommand.ml index e16f9dd197..479b04228e 100644 --- a/plugins/xml/xmlcommand.ml +++ b/plugins/xml/xmlcommand.ml @@ -289,7 +289,7 @@ let kind_of_variable id = | IsAssumption Conjectural -> "VARIABLE","Conjecture" | IsDefinition Definition -> "VARIABLE","LocalDefinition" | IsProof _ -> "VARIABLE","LocalFact" - | _ -> Errors.anomaly "Unsupported variable kind" + | _ -> Errors.anomaly (Pp.str "Unsupported variable kind") ;; let kind_of_constant kn = @@ -423,7 +423,7 @@ let print_ref qid fn = (* pretty prints via Xml.pp the proof in progress on dest *) let show_pftreestate internal fn (kind,pftst) id = if true then - Errors.anomaly "Xmlcommand.show_pftreestate is not supported in this version." + Errors.anomaly (Pp.str "Xmlcommand.show_pftreestate is not supported in this version.") let show fn = let pftst = Pfedit.get_pftreestate () in @@ -519,7 +519,7 @@ let _ = let options = " --html -s --body-only --no-index --latin1 --raw-comments" in let command cmd = if Sys.command cmd <> 0 then - Errors.anomaly ("Error executing \"" ^ cmd ^ "\"") + Errors.anomaly (Pp.str ("Error executing \"" ^ cmd ^ "\"")) in command (coqdoc^options^" -o "^fn^".xml "^fn^".v"); command ("rm "^fn^".v "^fn^".glob"); |