diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2018-07-05 12:56:27 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2018-07-05 12:56:27 +0200 |
| commit | d19605b7bfb8425b53be4cab30bef462c4fa4d14 (patch) | |
| tree | 2bdcc15e217c24ca33b2fe48537c8632562a9ec1 /printing/pputils.ml | |
| parent | 7413f8532879c64e05ee0e8ca16693d74fe84ab9 (diff) | |
| parent | 08b2fde7054a61e5468ef90eabb0d348730f170e (diff) | |
Merge PR #7746: Many small cleanups removing unused arguments and functions
Diffstat (limited to 'printing/pputils.ml')
| -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 ()) ++ |