aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/micromega
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 /plugins/micromega
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 'plugins/micromega')
-rw-r--r--plugins/micromega/g_micromega.ml42
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/micromega/g_micromega.ml4 b/plugins/micromega/g_micromega.ml4
index eb713f251..a17c62eba 100644
--- a/plugins/micromega/g_micromega.ml4
+++ b/plugins/micromega/g_micromega.ml4
@@ -20,7 +20,7 @@ open Errors
open Misctypes
let out_arg = function
- | ArgVar _ -> anomaly "Unevaluated or_var variable"
+ | ArgVar _ -> anomaly (Pp.str "Unevaluated or_var variable")
| ArgArg x -> x
TACTIC EXTEND PsatzZ