From 86c9c7cec60a2e302a317acadc559cb6e3c481f5 Mon Sep 17 00:00:00 2001
From: Yann Herklotz <git@yannherklotz.com>
Date: Tue, 12 Jan 2021 20:27:20 +0000
Subject: Remove unnecessary definition of check

---
 src/hls/Scheduleoracle.v | 10 ++++------
 1 file changed, 4 insertions(+), 6 deletions(-)

diff --git a/src/hls/Scheduleoracle.v b/src/hls/Scheduleoracle.v
index 09b1355..b5aa86d 100644
--- a/src/hls/Scheduleoracle.v
+++ b/src/hls/Scheduleoracle.v
@@ -1,3 +1,7 @@
+(*|
+.. coq:: none
+|*)
+
 (*
  * Vericert: Verified high-level synthesis.
  * Copyright (C) 2021 Yann Herklotz <yann@yannherklotz.com>
@@ -368,12 +372,6 @@ Definition empty : forest := Rtree.empty _.
 This function checks if all the elements in [fa] are in [fb], but not the other way round.
 |*)
 
-Definition check_partial (fa fb : forest) : bool :=
-  PTree.fold (fun b i el => b && (match PTree.get i fb with
-                                    | Some el' => beq_expression el el'
-                                    | None => false
-                                  end)) fa true.
-
 Definition check := Rtree.beq beq_expression.
 
 Lemma check_correct: forall (fa fb : forest) (x : resource),
-- 
cgit