aboutsummaryrefslogtreecommitdiff
path: root/src/PushButtonSynthesis/SaturatedSolinas.v
diff options
context:
space:
mode:
authorGravatar Jason Gross <jgross@mit.edu>2019-01-24 15:35:49 -0500
committerGravatar Jason Gross <jasongross9@gmail.com>2019-01-26 18:12:06 -0500
commit9b9adfa6437439cf133da6f062b0b6050a691cdf (patch)
tree7440a07ff5cad7936fb56dc6ae4cea2fc2dc05b2 /src/PushButtonSynthesis/SaturatedSolinas.v
parentef14767f91007ebf506f45f8d669a00f0b332345 (diff)
Also display the carry chain in a comment
Diffstat (limited to 'src/PushButtonSynthesis/SaturatedSolinas.v')
-rw-r--r--src/PushButtonSynthesis/SaturatedSolinas.v4
1 files changed, 2 insertions, 2 deletions
diff --git a/src/PushButtonSynthesis/SaturatedSolinas.v b/src/PushButtonSynthesis/SaturatedSolinas.v
index bcb93c4a1..334c2a475 100644
--- a/src/PushButtonSynthesis/SaturatedSolinas.v
+++ b/src/PushButtonSynthesis/SaturatedSolinas.v
@@ -176,9 +176,9 @@ Section __.
(** Note: If you change the name or type signature of this
function, you will need to update the code in CLI.v *)
Definition Synthesize (function_name_prefix : string) (requests : list string)
- : list (string * Pipeline.ErrorT (list string)) * PositiveSet.t (* types used *)
+ : list string * list (string * Pipeline.ErrorT (list string)) * PositiveSet.t (* types used *)
:= Primitives.Synthesize
machine_wordsize valid_names known_functions (fun _ => nil)
- function_name_prefix requests.
+ [] function_name_prefix requests.
End for_stringification.
End __.