Ignore:
Timestamp:
Dec 1, 2010, 6:03:45 PM (9 years ago)
Author:
mulligan
Message:

Do not use ndestruct for injectivity since it introduces StreickerK that
blocks reductions.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • Deliverables/D4.1/Matita/depends

    r344 r352  
    77Maybe.ma Bool.ma Plogic/equality.ma Universes.ma
    88Either.ma Bool.ma Maybe.ma Universes.ma
     9DoTest.ma Test.ma
    910ASM.ma BitVectorTrie.ma Either.ma String.ma
    1011Fetch.ma ASM.ma Arithmetic.ma BitVectorTrie.ma
    1112Char.ma Universes.ma
     13Test.ma Assembly.ma Interpret.ma
    1214Vector.ma Cartesian.ma List.ma Maybe.ma Nat.ma Plogic/equality.ma Util.ma
    1315Connectives.ma Plogic/equality.ma
Note: See TracChangeset for help on using the changeset viewer.