aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/micromega/g_micromega.ml4
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/micromega/g_micromega.ml4')
-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