diff options
Diffstat (limited to 'scheduling/BTLaux.ml')
| -rw-r--r-- | scheduling/BTLaux.ml | 3 |
1 files changed, 0 insertions, 3 deletions
diff --git a/scheduling/BTLaux.ml b/scheduling/BTLaux.ml deleted file mode 100644 index ca34c21c..00000000 --- a/scheduling/BTLaux.ml +++ /dev/null @@ -1,3 +0,0 @@ -type inst_info = { mutable inumb : int; mutable pcond : bool option } - -type block_info = { mutable bnumb : int; mutable visited : bool } |