diff options
| author |  Matej Kosik <m4tej.kosik@gmail.com> | 2015-12-16 16:19:51 +0100 |
|---|---|---|
| committer | Matej Kosik <m4tej.kosik@gmail.com> | 2016-01-11 14:59:26 +0100 |
| commit | a1aff01d16bad2f44392fd5cb804092e12e558ed (patch) | |
| tree | bd2a1faf08b1c399171a308cf45bfd46d60ab5c5 /printing | |
| parent | 78bad016e389cd78635d40281bfefd7136733b7e (diff) | |
CLEANUP: removing unused field
I have removed the second field of the "Constrexpr.CRecord" variant
because once it was set to "None"
it never changed to anything else.
It was just carried and copied around.
Diffstat (limited to 'printing')
| -rw-r--r-- | printing/ppconstr.ml | 12 |
1 files changed, 2 insertions, 10 deletions
diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml index c07057a09..334399782 100644 --- a/printing/ppconstr.ml +++ b/printing/ppconstr.ml @@ -593,17 +593,9 @@ end) = struct return (p, lproj) | CApp (_,(None,a),l) -> return (pr_app (pr mt) a l, lapp) - | CRecord (_,w,l) -> - let beg = - match w with - | None -> - spc () - | Some t -> - spc () ++ pr spc ltop t ++ spc () - ++ keyword "with" ++ spc () - in + | CRecord (_,l) -> return ( - hv 0 (str"{|" ++ beg ++ + hv 0 (str"{|" ++ spc () ++ prlist_with_sep pr_semicolon (fun (id, c) -> h 1 (pr_reference id ++ spc () ++ str":=" ++ pr spc ltop c)) l ++ str" |}"), |