diff options
| author | Gabriel Kerneis | 2014-05-15 12:41:53 +0100 |
|---|---|---|
| committer | Gabriel Kerneis | 2014-05-15 12:42:59 +0100 |
| commit | 98a61ad83f968d856d4f86ca32fcca8010a44f6f (patch) | |
| tree | 6edf2a270b5e29b40d2c11c497e7dc736db2e734 /src | |
| parent | f093aa8719cebbf17e7cbd279fa83376ef9b0bfb (diff) | |
Fix infinite loop bug
The output is *completely* broken (a mix of missing and too many
whitespaces). No idea what is going on.
Diffstat (limited to 'src')
| -rw-r--r-- | src/pretty_print.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/pretty_print.ml b/src/pretty_print.ml index c3eb6be2..2296dded 100644 --- a/src/pretty_print.ml +++ b/src/pretty_print.ml @@ -1052,7 +1052,7 @@ and doc_exp e = and starstar_exp ((E_aux(e,_)) as expr) = match e with | E_app_infix(l,(Id_aux(Id "**",_) as op),r) -> doc_op (doc_id op) (starstar_exp l) (app_exp r) - | _ -> star_exp expr + | _ -> app_exp expr and app_exp ((E_aux(e,_)) as expr) = match e with | E_app(f,args) -> doc_unop (doc_id f) (parens (separate_map comma exp args)) |