aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
-rw-r--r--printing/pputils.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/printing/pputils.ml b/printing/pputils.ml
index c6b8d5022..59e5f68f2 100644
--- a/printing/pputils.ml
+++ b/printing/pputils.ml
@@ -68,7 +68,7 @@ let pr_short_red_flag pr r =
let pr_red_flag pr r =
try pr_short_red_flag pr r
- with complexRedFlags ->
+ with ComplexRedFlag ->
(if r.rBeta then pr_arg str "beta" else mt ()) ++
(if r.rMatch && r.rFix && r.rCofix then pr_arg str "iota" else
(if r.rMatch then pr_arg str "match" else mt ()) ++