diff options
| author | Michalis Pardalos <m.pardalos@gmail.com> | 2021-08-30 22:15:02 +0100 |
|---|---|---|
| committer | Michalis Pardalos <m.pardalos@gmail.com> | 2021-08-30 22:15:02 +0100 |
| commit | 8bc6214e053aa4487abfbd895c00e2da9f21bd8a (patch) | |
| tree | 2301479ca921c014a57ca419fbeb32f17624e7e7 /src/hls/HTLgen.v | |
| parent | b067e5c7b0ecce9ffbf21e9c4a7ff96328dec2ba (diff) | |
| download | vericert-8bc6214e053aa4487abfbd895c00e2da9f21bd8a.tar.gz vericert-8bc6214e053aa4487abfbd895c00e2da9f21bd8a.zip | |
WIP
Diffstat (limited to 'src/hls/HTLgen.v')
| -rw-r--r-- | src/hls/HTLgen.v | 11 |
1 files changed, 0 insertions, 11 deletions
diff --git a/src/hls/HTLgen.v b/src/hls/HTLgen.v index 0b7f3ec..84e1a0f 100644 --- a/src/hls/HTLgen.v +++ b/src/hls/HTLgen.v @@ -626,17 +626,6 @@ Proof. simplify. transitivity (Z.pos (max_pc_map m)); eauto. Qed. -Definition decide_order a b c d e f g : {module_ordering a b c d e f g} + {True}. - refine (match bool_dec ((a <? b) && (b <? c) && (c <? d) - && (d <? e) && (e <? f) && (f <? g))%positive true with - | left t => left _ - | _ => _ - end); auto. - simplify; repeat match goal with - | H: context[(_ <? _)%positive] |- _ => apply Pos.ltb_lt in H - end; unfold module_ordering; auto. -Defined. - Definition transf_module (f: function) : mon HTL.module. refine ( if stack_correct f.(fn_stacksize) then |