diff options
| author |  Jason Gross <jgross@mit.edu> | 2019-02-01 18:50:00 -0500 |
|---|---|---|
| committer |  Jason Gross <jasongross9@gmail.com> | 2019-02-02 18:22:15 -0500 |
| commit | ce583d76bdb8f15148fc4222d8bdec096547682a (patch) | |
| tree | ffb083673e6be283d7f67ad857bc2f30af892767 /src/CStringification.v | |
| parent | 069e5cce23669707f11e59d9f68a31ad24990fe0 (diff) | |
Use Preconditions: Postconditions:, rather than /\ and ->
Diffstat (limited to 'src/CStringification.v')
| -rw-r--r-- | src/CStringification.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/CStringification.v b/src/CStringification.v index d31fa55e8..b50957dcd 100644 --- a/src/CStringification.v +++ b/src/CStringification.v @@ -2212,7 +2212,7 @@ Module Compilers. := match ExprOfPHOAS do_bounds_check e name_list inbounds with | inl (indata, outdata, f) => inl ((["/*"] - ++ (List.map (fun s => " * " ++ s)%string (comment indata outdata)) + ++ (List.map (fun s => if (String.length s =? 0)%nat then " *" else (" * " ++ s))%string (comment indata outdata)) ++ [" * Input Bounds:"] ++ List.map (fun v => " * " ++ v)%string (input_bounds_to_string indata inbounds) ++ [" * Output Bounds:"] |