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

    r2717 r2773  
    122122let rec check_be_null n = function
    123123| List.Nil -> Nat.eqb AST.size_pointer n
    124 | List.Cons (hd0, tl) ->
    125   (match hd0 with
     124| List.Cons (hd, tl) ->
     125  (match hd with
    126126   | ByteValues.BVundef -> Bool.False
    127127   | ByteValues.BVnonzero -> Bool.False
     
    152152        | ByteValues.BVByte b ->
    153153          Types.option_map (fun tl ->
    154             Vector.append0 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
     154            Vector.append (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    155155              (Nat.S Nat.O))))))))
    156156              (Nat.times m (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
Note: See TracChangeset for help on using the changeset viewer.