aboutsummaryrefslogtreecommitdiff
path: root/src/PushButtonSynthesis/SaturatedSolinas.v
diff options
context:
space:
mode:
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 __.