Changeset 2773 for extracted/costSpec.ml


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

    r2730 r2773  
    11open Preamble
     2
     3open BitVectorTrie
    24
    35open Graphs
     
    3133open FrontEndOps
    3234
    33 open BitVectorTrie
    34 
    3535open CostLabel
    3636
     
    4949open Extralib
    5050
    51 open Setoids
    52 
    53 open Monad
    54 
    55 open Option
    56 
    5751open Lists
    5852
     
    6963open Div_and_mod
    7064
     65open Util
     66
     67open FoldStuff
     68
     69open BitVector
     70
    7171open Jmeq
    7272
     
    7575open List
    7676
    77 open Util
     77open Setoids
    7878
    79 open FoldStuff
     79open Monad
    8080
    81 open BitVector
     81open Option
    8282
    8383open Extranat
     
    137137    RTLabs_syntax.statement Graphs.graph -> RTLabs_syntax.statement ->
    138138    Bool.bool **)
    139 let well_cost_labelled_statement g0 s =
     139let well_cost_labelled_statement g s =
    140140  (match s with
    141141   | RTLabs_syntax.St_skip x -> (fun _ -> Bool.True)
     
    153153       Bool.andb
    154154         (is_cost_label
    155            (Identifiers.lookup_present PreIdentifiers.LabelTag g0 l1))
     155           (Identifiers.lookup_present PreIdentifiers.LabelTag g l1))
    156156         (is_cost_label
    157            (Identifiers.lookup_present PreIdentifiers.LabelTag g0 l2)))
     157           (Identifiers.lookup_present PreIdentifiers.LabelTag g l2)))
    158158   | RTLabs_syntax.St_return -> (fun _ -> Bool.True)) __
    159159
Note: See TracChangeset for help on using the changeset viewer.