X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=extracted%2Ffetch.mli;h=283dc7f8501ed5ecb6f43fd0af6a154bea0d169a;hb=HEAD;hp=bad649da146ff50f8d38c6cb60b031386004362b;hpb=69b6010f0016bba47bc7e74ad8e1f3fa473f259f;p=pkg-cerco%2Facc-trusted.git

diff --git a/extracted/fetch.mli b/extracted/fetch.mli
index bad649d..283dc7f 100644
--- a/extracted/fetch.mli
+++ b/extracted/fetch.mli
@@ -1,5 +1,19 @@
 open Preamble
 
+open Types
+
+open Hints_declaration
+
+open Core_notation
+
+open Pts
+
+open Logic
+
+open Jmeq
+
+open Russell
+
 open Exp
 
 open Setoids
@@ -14,12 +28,6 @@ open Vector
 
 open Div_and_mod
 
-open Jmeq
-
-open Russell
-
-open Types
-
 open List
 
 open Util
@@ -28,14 +36,6 @@ open FoldStuff
 
 open Bool
 
-open Hints_declaration
-
-open Core_notation
-
-open Pts
-
-open Logic
-
 open Relations
 
 open Nat
@@ -78,26 +78,22 @@ open CostLabel
 
 open ASM
 
-val inefficient_address_of_word_labels_code_mem :
-  ASM.labelled_instruction List.list -> ASM.identifier -> BitVector.bitVector
+val inefficient_address_of_label :
+  ASM.labelled_instruction List.list -> ASM.identifier -> Nat.nat
 
 type label_map = Nat.nat Identifiers.identifier_map
 
 val create_label_cost_map0 :
-  ASM.labelled_instruction List.list -> (label_map, CostLabel.costlabel
-  BitVectorTrie.bitVectorTrie) Types.prod Types.sig0
+  ASM.labelled_instruction List.list -> (label_map, ASM.costlabel_map)
+  Types.prod Types.sig0
 
 val create_label_cost_map :
-  ASM.labelled_instruction List.list -> (label_map, CostLabel.costlabel
-  BitVectorTrie.bitVectorTrie) Types.prod
+  ASM.labelled_instruction List.list -> (label_map, ASM.costlabel_map)
+  Types.prod
 
 val address_of_word_labels :
   ASM.labelled_instruction List.list -> ASM.identifier -> BitVector.word
 
-val bitvector_max_nat : Nat.nat -> Nat.nat
-
-val code_memory_size : Nat.nat
-
 val prod_inv_rect_Type0 :
   ('a1, 'a2) Types.prod -> ('a1 -> 'a2 -> __ -> 'a3) -> 'a3