aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
authorGravatar Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>2017-09-05 15:37:10 +0200
committerGravatar Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>2018-07-03 13:39:18 +0200
commitf61d86f83b701ae3ce3d7f542325e0bfa4c8d810 (patch)
treed11cd2706bb08113470500d716285339d6302a6c
parent8baf4746c931c29a04a3c7eced71743ad3e608bf (diff)
Pputils: fix typo
-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 ()) ++