diff options
| author |  Robert Sloan <varomodt@gmail.com> | 2016-06-23 19:45:15 -0400 |
|---|---|---|
| committer | Robert Sloan <varomodt@gmail.com> | 2016-06-23 19:45:15 -0400 |
| commit | 1729cd4d6f471096642a22aa789f47bc5792beba (patch) | |
| tree | 343066ca2c40ac9290b67a8079f045c62ec2f55a /src/Assembly | |
| parent | 14f41f622196bafcd9ad40543f21b72d88e01e7d (diff) | |
Remove examples for 8.4 compatibility
Diffstat (limited to 'src/Assembly')
| -rw-r--r-- | src/Assembly/Pipeline.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/Assembly/Pipeline.v b/src/Assembly/Pipeline.v index 97aa94d36..8e58e7345 100644 --- a/src/Assembly/Pipeline.v +++ b/src/Assembly/Pipeline.v @@ -27,6 +27,7 @@ Module PipelineExamples. Local Notation "v [[ i ]]" := (nth i v (wzero _)) (at level 40). Local Notation "$$ v" := (natToWord _ v) (at level 40). + (* Definition add_example: @pseudeq 32 W32 1 1 (fun v => plet a := $$ 1 in plet b := v[[0]] in @@ -63,7 +64,6 @@ Module PipelineExamples. Definition mult_ex_str := (Pipeline.toString (proj1_sig mult_example)). - (* Definition comb_example: @pseudeq 32 W32 1 1 (fun v => plet a := $$ 7 in plet b := v[[0]] in |