diff options
| author |  Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2017-09-05 15:37:10 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2018-07-03 13:39:18 +0200 |
| commit | f61d86f83b701ae3ce3d7f542325e0bfa4c8d810 (patch) | |
| tree | d11cd2706bb08113470500d716285339d6302a6c | |
| parent | 8baf4746c931c29a04a3c7eced71743ad3e608bf (diff) | |
Pputils: fix typo
| -rw-r--r-- | printing/pputils.ml | 2 |
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 ()) ++ |