aboutsummaryrefslogtreecommitdiffhomepage
path: root/printing/printmod.ml
diff options
context:
space:
mode:
authorGravatar ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7>2013-01-28 21:05:35 +0000
committerGravatar ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7>2013-01-28 21:05:35 +0000
commit5a39e6c08d428d774165e0ef3922ba8b75eee9e1 (patch)
treee035f490e2c748356df73342876b22cfcb3bc5a0 /printing/printmod.ml
parent5e8824960f68f529869ac299b030282cc916ba2c (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 'printing/printmod.ml')
-rw-r--r--printing/printmod.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/printing/printmod.ml b/printing/printmod.ml
index 2b0f458c1..5980dae0c 100644
--- a/printing/printmod.ml
+++ b/printing/printmod.ml
@@ -203,7 +203,7 @@ let rec print_modexpr env mp locals mexpr = match mexpr with
| SEBapply _ ->
let lapp = flatten_app mexpr [] in
hov 3 (str"(" ++ prlist_with_sep spc (print_modpath locals) lapp ++ str")")
- | SEBwith (_,_)-> anomaly "Not available yet"
+ | SEBwith (_,_)-> anomaly (Pp.str "Not available yet")
let rec printable_body dir =