Ignore:
Timestamp:
Mar 4, 2013, 10:03:33 AM (8 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/memoryInjections.mli

    r2717 r2773  
    4747open Csem
    4848
    49 open BitVectorTrie
    50 
    5149open CostLabel
    5250
    … …  
    6765open Extralib
    6866
    69 open Setoids
    70 
    71 open Monad
    72 
    73 open Option
    74 
    7567open Lists
    7668
    … …  
    8779open Div_and_mod
    8880
     81open Util
     82
     83open FoldStuff
     84
     85open BitVector
     86
    8987open Jmeq
    9088
    … …  
    9391open List
    9492
    95 open Util
     93open Setoids
    9694
    97 open FoldStuff
     95open Monad
    9896
    99 open BitVector
     97open Option
    10098
    10199open Extranat
    … …  
    145143
    146144val memory_inj_rect_Type4 :
    147   embedding -> GenMem.mem1 -> GenMem.mem1 -> (__ -> __ -> __ -> __ -> __ ->
    148   __ -> __ -> 'a1) -> 'a1
     145  embedding -> GenMem.mem -> GenMem.mem -> (__ -> __ -> __ -> __ -> __ -> __
     146  -> __ -> 'a1) -> 'a1
    149147
    150148val memory_inj_rect_Type5 :
    151   embedding -> GenMem.mem1 -> GenMem.mem1 -> (__ -> __ -> __ -> __ -> __ ->
    152   __ -> __ -> 'a1) -> 'a1
     149  embedding -> GenMem.mem -> GenMem.mem -> (__ -> __ -> __ -> __ -> __ -> __
     150  -> __ -> 'a1) -> 'a1
    153151
    154152val memory_inj_rect_Type3 :
    155   embedding -> GenMem.mem1 -> GenMem.mem1 -> (__ -> __ -> __ -> __ -> __ ->
    156   __ -> __ -> 'a1) -> 'a1
     153  embedding -> GenMem.mem -> GenMem.mem -> (__ -> __ -> __ -> __ -> __ -> __
     154  -> __ -> 'a1) -> 'a1
    157155
    158156val memory_inj_rect_Type2 :
    159   embedding -> GenMem.mem1 -> GenMem.mem1 -> (__ -> __ -> __ -> __ -> __ ->
    160   __ -> __ -> 'a1) -> 'a1
     157  embedding -> GenMem.mem -> GenMem.mem -> (__ -> __ -> __ -> __ -> __ -> __
     158  -> __ -> 'a1) -> 'a1
    161159
    162160val memory_inj_rect_Type1 :
    163   embedding -> GenMem.mem1 -> GenMem.mem1 -> (__ -> __ -> __ -> __ -> __ ->
    164   __ -> __ -> 'a1) -> 'a1
     161  embedding -> GenMem.mem -> GenMem.mem -> (__ -> __ -> __ -> __ -> __ -> __
     162  -> __ -> 'a1) -> 'a1
    165163
    166164val memory_inj_rect_Type0 :
    167   embedding -> GenMem.mem1 -> GenMem.mem1 -> (__ -> __ -> __ -> __ -> __ ->
    168   __ -> __ -> 'a1) -> 'a1
     165  embedding -> GenMem.mem -> GenMem.mem -> (__ -> __ -> __ -> __ -> __ -> __
     166  -> __ -> 'a1) -> 'a1
    169167
    170168val memory_inj_inv_rect_Type4 :
    171   embedding -> GenMem.mem1 -> GenMem.mem1 -> (__ -> __ -> __ -> __ -> __ ->
    172   __ -> __ -> __ -> 'a1) -> 'a1
     169  embedding -> GenMem.mem -> GenMem.mem -> (__ -> __ -> __ -> __ -> __ -> __
     170  -> __ -> __ -> 'a1) -> 'a1
    173171
    174172val memory_inj_inv_rect_Type3 :
    175   embedding -> GenMem.mem1 -> GenMem.mem1 -> (__ -> __ -> __ -> __ -> __ ->
    176   __ -> __ -> __ -> 'a1) -> 'a1
     173  embedding -> GenMem.mem -> GenMem.mem -> (__ -> __ -> __ -> __ -> __ -> __
     174  -> __ -> __ -> 'a1) -> 'a1
    177175
    178176val memory_inj_inv_rect_Type2 :
    179   embedding -> GenMem.mem1 -> GenMem.mem1 -> (__ -> __ -> __ -> __ -> __ ->
    180   __ -> __ -> __ -> 'a1) -> 'a1
     177  embedding -> GenMem.mem -> GenMem.mem -> (__ -> __ -> __ -> __ -> __ -> __
     178  -> __ -> __ -> 'a1) -> 'a1
    181179
    182180val memory_inj_inv_rect_Type1 :
    183   embedding -> GenMem.mem1 -> GenMem.mem1 -> (__ -> __ -> __ -> __ -> __ ->
    184   __ -> __ -> __ -> 'a1) -> 'a1
     181  embedding -> GenMem.mem -> GenMem.mem -> (__ -> __ -> __ -> __ -> __ -> __
     182  -> __ -> __ -> 'a1) -> 'a1
    185183
    186184val memory_inj_inv_rect_Type0 :
    187   embedding -> GenMem.mem1 -> GenMem.mem1 -> (__ -> __ -> __ -> __ -> __ ->
    188   __ -> __ -> __ -> 'a1) -> 'a1
     185  embedding -> GenMem.mem -> GenMem.mem -> (__ -> __ -> __ -> __ -> __ -> __
     186  -> __ -> __ -> 'a1) -> 'a1
    189187
    190 val memory_inj_jmdiscr : embedding -> GenMem.mem1 -> GenMem.mem1 -> __
     188val memory_inj_jmdiscr : embedding -> GenMem.mem -> GenMem.mem -> __
    191189
    192190val typesize' : Csyntax.type0 -> Nat.nat
Note: See TracChangeset for help on using the changeset viewer.