Changeset 2773 for extracted/fetch.mli


Ignore:
Timestamp:
Mar 4, 2013, 10:03:33 AM (7 years ago)
Author:
sacerdot
Message:
  1. everything extracted again after all bugs in Matita's extraction have been fixed. No more need for manual patching
  2. new extraction after file reorganization (by James)
File:
1 edited

Legend:

Unmodified
Added
Removed
  • extracted/fetch.mli

    r2717 r2773  
    11open Preamble
     2
     3open Exp
     4
     5open Setoids
     6
     7open Monad
     8
     9open Option
    210
    311open Extranat
     
    1119open Russell
    1220
     21open Types
     22
    1323open List
    1424
     
    1828
    1929open Bool
    20 
    21 open Relations
    22 
    23 open Nat
    24 
    25 open BitVector
    2630
    2731open Hints_declaration
     
    3337open Logic
    3438
    35 open Types
     39open Relations
     40
     41open Nat
     42
     43open BitVector
     44
     45open Arithmetic
    3646
    3747open BitVectorTrie
    3848
    39 open Exp
    40 
    41 open Arithmetic
    42 
    4349open String
    44 
    45 open LabelledObjects
    4650
    4751open Integers
     
    4953open AST
    5054
    51 open CostLabel
     55open LabelledObjects
    5256
    5357open Proper
     
    6569open Extralib
    6670
    67 open Setoids
    68 
    69 open Monad
    70 
    71 open Option
    72 
    7371open Lists
    7472
     
    7775open Identifiers
    7876
     77open CostLabel
     78
    7979open ASM
    8080
    8181val inefficient_address_of_word_labels_code_mem :
    82   ASM.labelled_instruction List.list -> ASM.identifier0 ->
    83   BitVector.bitVector
     82  ASM.labelled_instruction List.list -> ASM.identifier -> BitVector.bitVector
    8483
    8584type label_map = Nat.nat Identifiers.identifier_map
     
    9493
    9594val address_of_word_labels :
    96   ASM.labelled_instruction List.list -> ASM.identifier0 -> BitVector.word
     95  ASM.labelled_instruction List.list -> ASM.identifier -> BitVector.word
    9796
    9897val bitvector_max_nat : Nat.nat -> Nat.nat
     
    105104
    106105val load_code_memory0 :
    107   BitVector.byte List.list -> BitVector.byte BitVectorTrie.bitVectorTrie
    108   Types.sig0
     106  ASM.object_code -> BitVector.byte BitVectorTrie.bitVectorTrie Types.sig0
    109107
    110108val load_code_memory :
    111   BitVector.byte List.list -> BitVector.byte BitVectorTrie.bitVectorTrie
     109  ASM.object_code -> BitVector.byte BitVectorTrie.bitVectorTrie
    112110
    113 val prod_inv_rect_Type5 :
     111val prod_inv_rect_Type0 :
    114112  ('a1, 'a2) Types.prod -> ('a1 -> 'a2 -> __ -> 'a3) -> 'a3
    115113
Note: See TracChangeset for help on using the changeset viewer.