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