diff options
Diffstat (limited to 'src/Assembly/PipelineExample.v')
| -rw-r--r-- | src/Assembly/PipelineExample.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/Assembly/PipelineExample.v b/src/Assembly/PipelineExample.v index d4cd4d142..b17a85c9b 100644 --- a/src/Assembly/PipelineExample.v +++ b/src/Assembly/PipelineExample.v @@ -45,4 +45,4 @@ Module Progs. Print result. End Progs. -(* Extraction "Progs.ml" Progs. *) +Extraction "Progs.ml" Progs. |