From 8bc6214e053aa4487abfbd895c00e2da9f21bd8a Mon Sep 17 00:00:00 2001
From: Michalis Pardalos <m.pardalos@gmail.com>
Date: Mon, 30 Aug 2021 22:15:02 +0100
Subject: WIP

---
 src/hls/HTLgen.v | 11 -----------
 1 file changed, 11 deletions(-)

(limited to 'src/hls/HTLgen.v')

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
-- 
cgit