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

    r2717 r2773  
    11open Preamble
    22
    3 open BitVectorTrie
    4 
    53open CostLabel
    64
     
    2119open Extralib
    2220
     21open Lists
     22
     23open Positive
     24
     25open Identifiers
     26
     27open Exp
     28
     29open Arithmetic
     30
     31open Vector
     32
     33open Div_and_mod
     34
     35open Util
     36
     37open FoldStuff
     38
     39open BitVector
     40
     41open Jmeq
     42
     43open Russell
     44
     45open List
     46
    2347open Setoids
    2448
     
    2650
    2751open Option
    28 
    29 open Lists
    30 
    31 open Positive
    32 
    33 open Identifiers
    34 
    35 open Exp
    36 
    37 open Arithmetic
    38 
    39 open Vector
    40 
    41 open Div_and_mod
    42 
    43 open Jmeq
    44 
    45 open Russell
    46 
    47 open List
    48 
    49 open Util
    50 
    51 open FoldStuff
    52 
    53 open BitVector
    5452
    5553open Extranat
     
    177175val simplify_program : Csyntax.clight_program -> Csyntax.clight_program
    178176
    179 val related_globals_rect_Type6 :
    180   ('a1 -> 'a1) -> 'a1 Globalenvs.genv_t -> 'a1 Globalenvs.genv_t -> (__ -> __
    181   -> __ -> 'a2) -> 'a2
    182 
    183 val related_globals_rect_Type7 :
    184   ('a1 -> 'a1) -> 'a1 Globalenvs.genv_t -> 'a1 Globalenvs.genv_t -> (__ -> __
    185   -> __ -> 'a2) -> 'a2
    186 
    187 val related_globals_rect_Type8 :
    188   ('a1 -> 'a1) -> 'a1 Globalenvs.genv_t -> 'a1 Globalenvs.genv_t -> (__ -> __
    189   -> __ -> 'a2) -> 'a2
    190 
    191 val related_globals_rect_Type9 :
    192   ('a1 -> 'a1) -> 'a1 Globalenvs.genv_t -> 'a1 Globalenvs.genv_t -> (__ -> __
    193   -> __ -> 'a2) -> 'a2
    194 
    195 val related_globals_rect_Type10 :
    196   ('a1 -> 'a1) -> 'a1 Globalenvs.genv_t -> 'a1 Globalenvs.genv_t -> (__ -> __
    197   -> __ -> 'a2) -> 'a2
    198 
    199 val related_globals_rect_Type11 :
    200   ('a1 -> 'a1) -> 'a1 Globalenvs.genv_t -> 'a1 Globalenvs.genv_t -> (__ -> __
    201   -> __ -> 'a2) -> 'a2
    202 
    203 val related_globals_inv_rect_Type5 :
    204   ('a1 -> 'a1) -> 'a1 Globalenvs.genv_t -> 'a1 Globalenvs.genv_t -> (__ -> __
    205   -> __ -> __ -> 'a2) -> 'a2
    206 
    207 val related_globals_inv_rect_Type6 :
    208   ('a1 -> 'a1) -> 'a1 Globalenvs.genv_t -> 'a1 Globalenvs.genv_t -> (__ -> __
    209   -> __ -> __ -> 'a2) -> 'a2
    210 
    211 val related_globals_inv_rect_Type7 :
    212   ('a1 -> 'a1) -> 'a1 Globalenvs.genv_t -> 'a1 Globalenvs.genv_t -> (__ -> __
    213   -> __ -> __ -> 'a2) -> 'a2
    214 
    215 val related_globals_inv_rect_Type8 :
    216   ('a1 -> 'a1) -> 'a1 Globalenvs.genv_t -> 'a1 Globalenvs.genv_t -> (__ -> __
    217   -> __ -> __ -> 'a2) -> 'a2
    218 
    219 val related_globals_inv_rect_Type9 :
    220   ('a1 -> 'a1) -> 'a1 Globalenvs.genv_t -> 'a1 Globalenvs.genv_t -> (__ -> __
    221   -> __ -> __ -> 'a2) -> 'a2
    222 
    223 val related_globals_discr0 :
     177val related_globals_rect_Type4 :
     178  ('a1 -> 'a1) -> 'a1 Globalenvs.genv_t -> 'a1 Globalenvs.genv_t -> (__ -> __
     179  -> __ -> 'a2) -> 'a2
     180
     181val related_globals_rect_Type5 :
     182  ('a1 -> 'a1) -> 'a1 Globalenvs.genv_t -> 'a1 Globalenvs.genv_t -> (__ -> __
     183  -> __ -> 'a2) -> 'a2
     184
     185val related_globals_rect_Type3 :
     186  ('a1 -> 'a1) -> 'a1 Globalenvs.genv_t -> 'a1 Globalenvs.genv_t -> (__ -> __
     187  -> __ -> 'a2) -> 'a2
     188
     189val related_globals_rect_Type2 :
     190  ('a1 -> 'a1) -> 'a1 Globalenvs.genv_t -> 'a1 Globalenvs.genv_t -> (__ -> __
     191  -> __ -> 'a2) -> 'a2
     192
     193val related_globals_rect_Type1 :
     194  ('a1 -> 'a1) -> 'a1 Globalenvs.genv_t -> 'a1 Globalenvs.genv_t -> (__ -> __
     195  -> __ -> 'a2) -> 'a2
     196
     197val related_globals_rect_Type0 :
     198  ('a1 -> 'a1) -> 'a1 Globalenvs.genv_t -> 'a1 Globalenvs.genv_t -> (__ -> __
     199  -> __ -> 'a2) -> 'a2
     200
     201val related_globals_inv_rect_Type4 :
     202  ('a1 -> 'a1) -> 'a1 Globalenvs.genv_t -> 'a1 Globalenvs.genv_t -> (__ -> __
     203  -> __ -> __ -> 'a2) -> 'a2
     204
     205val related_globals_inv_rect_Type3 :
     206  ('a1 -> 'a1) -> 'a1 Globalenvs.genv_t -> 'a1 Globalenvs.genv_t -> (__ -> __
     207  -> __ -> __ -> 'a2) -> 'a2
     208
     209val related_globals_inv_rect_Type2 :
     210  ('a1 -> 'a1) -> 'a1 Globalenvs.genv_t -> 'a1 Globalenvs.genv_t -> (__ -> __
     211  -> __ -> __ -> 'a2) -> 'a2
     212
     213val related_globals_inv_rect_Type1 :
     214  ('a1 -> 'a1) -> 'a1 Globalenvs.genv_t -> 'a1 Globalenvs.genv_t -> (__ -> __
     215  -> __ -> __ -> 'a2) -> 'a2
     216
     217val related_globals_inv_rect_Type0 :
     218  ('a1 -> 'a1) -> 'a1 Globalenvs.genv_t -> 'a1 Globalenvs.genv_t -> (__ -> __
     219  -> __ -> __ -> 'a2) -> 'a2
     220
     221val related_globals_discr :
    224222  ('a1 -> 'a1) -> 'a1 Globalenvs.genv_t -> 'a1 Globalenvs.genv_t -> __
    225223
    226 val related_globals_jmdiscr0 :
     224val related_globals_jmdiscr :
    227225  ('a1 -> 'a1) -> 'a1 Globalenvs.genv_t -> 'a1 Globalenvs.genv_t -> __
    228226
Note: See TracChangeset for help on using the changeset viewer.