From 496271f86e9dc6df1b23a189d6b8fd2a82db33aa Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Wed, 30 Jan 2019 19:13:27 -0500 Subject: Add autogenerated docstrings to synthesized code We now stringify the correctness conditions to generate docstrings for the synthesized code. Closes #512 Time commitment: about 6 hours --- src/PushButtonSynthesis/BarrettReduction.v | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) (limited to 'src/PushButtonSynthesis/BarrettReduction.v') diff --git a/src/PushButtonSynthesis/BarrettReduction.v b/src/PushButtonSynthesis/BarrettReduction.v index 3e3e4e105..bc525412a 100644 --- a/src/PushButtonSynthesis/BarrettReduction.v +++ b/src/PushButtonSynthesis/BarrettReduction.v @@ -91,7 +91,10 @@ Section rbarrett_red. Definition sbarrett_red (prefix : string) : string * (Pipeline.ErrorT (list string * ToString.C.ident_infos)) - := Eval cbv beta in FromPipelineToString prefix "barrett_red" barrett_red. + := Eval cbv beta in + FromPipelineToString + prefix "barrett_red" barrett_red + (fun _ _ _ => @nil string). (* TODO: Replace the following lemmas with a new-glue-style correctness lemma, like << -- cgit v1.2.3