Changeset 2773 for extracted/status.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/status.mli

    r2717 r2773  
    11open Preamble
    22
     3open BitVectorTrie
     4
    35open String
    46
     7open Exp
     8
     9open Arithmetic
     10
     11open Vector
     12
     13open FoldStuff
     14
     15open BitVector
     16
     17open Extranat
     18
     19open Integers
     20
     21open AST
     22
    523open LabelledObjects
    624
    7 open BitVectorTrie
    8 
    9 open Exp
    10 
    11 open Arithmetic
    12 
    13 open Integers
    14 
    15 open AST
     25open Proper
     26
     27open PositiveMap
     28
     29open Deqsets
     30
     31open ErrorMessages
     32
     33open PreIdentifiers
     34
     35open Errors
     36
     37open Extralib
     38
     39open Setoids
     40
     41open Monad
     42
     43open Option
     44
     45open Div_and_mod
     46
     47open Jmeq
     48
     49open Russell
     50
     51open Util
     52
     53open List
     54
     55open Lists
     56
     57open Bool
     58
     59open Relations
     60
     61open Nat
     62
     63open Positive
     64
     65open Hints_declaration
     66
     67open Core_notation
     68
     69open Pts
     70
     71open Logic
     72
     73open Types
     74
     75open Identifiers
    1676
    1777open CostLabel
    18 
    19 open Proper
    20 
    21 open PositiveMap
    22 
    23 open Deqsets
    24 
    25 open ErrorMessages
    26 
    27 open PreIdentifiers
    28 
    29 open Errors
    30 
    31 open Extralib
    32 
    33 open Setoids
    34 
    35 open Monad
    36 
    37 open Option
    38 
    39 open Lists
    40 
    41 open Positive
    42 
    43 open Identifiers
    44 
    45 open Extranat
    46 
    47 open Vector
    48 
    49 open Div_and_mod
    50 
    51 open Jmeq
    52 
    53 open Russell
    54 
    55 open Types
    56 
    57 open List
    58 
    59 open Util
    60 
    61 open FoldStuff
    62 
    63 open Bool
    64 
    65 open Hints_declaration
    66 
    67 open Core_notation
    68 
    69 open Pts
    70 
    71 open Logic
    72 
    73 open Relations
    74 
    75 open Nat
    76 
    77 open BitVector
    7878
    7979open ASM
     
    134134
    135135type lineType =
    136 | P2 of BitVector.byte
     136| P1 of BitVector.byte
    137137| P3 of BitVector.byte
    138138| SerialBuffer of serialBufferType
     
    539539  preStatus
    540540
    541 val fetch_pseudo_instruction :
    542   ASM.labelled_instruction List.list -> BitVector.word ->
    543   (ASM.pseudo_instruction, BitVector.word) Types.prod
    544 
    545541val construct_datalabels :
    546   ASM.preamble -> BitVector.word Identifiers.identifier_map
    547 
     542  (ASM.identifier, BitVector.word) Types.prod List.list -> BitVector.word
     543  Identifiers.identifier_map
     544
Note: See TracChangeset for help on using the changeset viewer.