diff options
| author | Yann Herklotz <git@yannherklotz.com> | 2020-03-29 16:41:09 +0100 |
|---|---|---|
| committer | Yann Herklotz <git@yannherklotz.com> | 2020-03-29 16:41:09 +0100 |
| commit | 65f30c5524280b5639a94674828986f0635b2477 (patch) | |
| tree | be05fd2acf456773a02dbc8a61135f9c187bc46e /src/translation | |
| parent | c3106c7a61ecb79c1f1be0922aef32dffc92cc41 (diff) | |
| download | vericert-65f30c5524280b5639a94674828986f0635b2477.tar.gz vericert-65f30c5524280b5639a94674828986f0635b2477.zip | |
Remove unnecessary examples from HTL
Diffstat (limited to 'src/translation')
| -rw-r--r-- | src/translation/HTLgen.v | 7 |
1 files changed, 1 insertions, 6 deletions
diff --git a/src/translation/HTLgen.v b/src/translation/HTLgen.v index 9c2e168..d7f88c1 100644 --- a/src/translation/HTLgen.v +++ b/src/translation/HTLgen.v @@ -17,8 +17,8 @@ *) From coqup Require Import HTL Coquplib. -From compcert Require Import Maps. +From compcert Require Import Maps. From compcert Require Errors. From compcert Require Import AST RTL. @@ -179,11 +179,6 @@ Definition transf_function (f: function) : Errors.res module := | Error err => Errors.Error err end. -Definition example : mon HTL.code := PTree.traverse transf_instr - (PTree.set 2%positive (RTL.Icall sig ros args res n) (PTree.set 1%positive (RTL.Iop (Op.Omove) nil 1%positive 2%positive) (PTree.empty RTL.instruction))). - -Compute example. - Definition transf_fundef (fd: fundef) : Errors.res moddecl := transf_partial_fundef transf_function fd. |