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/interpret.mli

    r2717 r2773  
    11open Preamble
    22
    3 open Deqsets
    4 
    5 open Sets
    6 
    7 open Bool
    8 
    9 open Relations
    10 
    11 open Nat
    12 
    13 open Hints_declaration
    14 
    15 open Core_notation
    16 
    17 open Pts
    18 
    19 open Logic
    20 
    21 open Types
    22 
    23 open List
    24 
    25 open Listb
     3open BitVectorTrie
    264
    275open String
    28 
    29 open LabelledObjects
    30 
    31 open BitVectorTrie
    326
    337open Exp
     
    359open Arithmetic
    3610
     11open Vector
     12
     13open FoldStuff
     14
     15open BitVector
     16
     17open Extranat
     18
    3719open Integers
    3820
    3921open AST
    4022
    41 open CostLabel
     23open LabelledObjects
    4224
    4325open Proper
    4426
    4527open PositiveMap
     28
     29open Deqsets
    4630
    4731open ErrorMessages
     
    5943open Option
    6044
    61 open Lists
    62 
    63 open Positive
    64 
    65 open Identifiers
    66 
    67 open Extranat
    68 
    69 open Vector
    70 
    7145open Div_and_mod
    7246
     
    7751open Util
    7852
    79 open FoldStuff
     53open List
    8054
    81 open BitVector
     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
     76
     77open CostLabel
    8278
    8379open ASM
     
    8884
    8985open Fetch
     86
     87open Hide
     88
     89open Division
     90
     91open Z
     92
     93open BitVectorZ
     94
     95open Pointers
     96
     97open Coqlib
     98
     99open Values
     100
     101open Events
     102
     103open IOMonad
     104
     105open IO
     106
     107open Sets
     108
     109open Listb
    90110
    91111open StructuredTraces
     
    136156
    137157val execute_1_pseudo_instruction :
    138   (ASM.preamble, ASM.labelled_instruction List.list) Types.prod ->
    139   (BitVector.word -> __ -> (Nat.nat, Nat.nat) Types.prod) ->
    140   Status.pseudoStatus -> Status.pseudoStatus
     158  ASM.pseudo_assembly_program -> (BitVector.word -> __ -> (Nat.nat, Nat.nat)
     159  Types.prod) -> Status.pseudoStatus -> Status.pseudoStatus
    141160
    142161val execute :
Note: See TracChangeset for help on using the changeset viewer.