aboutsummaryrefslogtreecommitdiff
path: root/src/Assembly/Pipeline.v
diff options
context:
space:
mode:
authorGravatar Robert Sloan <varomodt@gmail.com>2016-06-23 18:17:35 -0400
committerGravatar Robert Sloan <varomodt@gmail.com>2016-06-23 18:17:35 -0400
commit00d3d987c065ba80becb02d5923f71184fdaa0cc (patch)
tree19a483d40a18113832b5d4fdfd0f5841d37360a3 /src/Assembly/Pipeline.v
parent2e760539d15eafeb7ed7018680d9436e4404de34 (diff)
Make Pipeline.v Build on 8.4
Diffstat (limited to 'src/Assembly/Pipeline.v')
-rw-r--r--src/Assembly/Pipeline.v4
1 files changed, 3 insertions, 1 deletions
diff --git a/src/Assembly/Pipeline.v b/src/Assembly/Pipeline.v
index ceb98a3a2..97aa94d36 100644
--- a/src/Assembly/Pipeline.v
+++ b/src/Assembly/Pipeline.v
@@ -63,14 +63,16 @@ 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
([b ^& a; a ^+ b])).
pseudo_solve.
- Admitted. (* TODO (rsloan): eapply unification *)
+ Admitted.
Definition comb_ex_str :=
(Pipeline.toString (proj1_sig comb_example)).
+ *)
End PipelineExamples.