source: Deliverables/D4.1/Matita/depends @ 352

Last change on this file since 352 was 352, checked in by mulligan, 9 years ago

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

File size: 1.0 KB
RevLine 
[344]1Exponential.ma Connectives.ma Nat.ma Plogic/equality.ma
2Status.ma ASM.ma Arithmetic.ma BitVectorTrie.ma
[341]3Arithmetic.ma BitVector.ma Bool.ma Connectives.ma Exponential.ma List.ma Nat.ma Plogic/equality.ma Universes.ma
[260]4BitVectorTrie.ma BitVector.ma Bool.ma Maybe.ma
5Cartesian.ma Universes.ma
[344]6Universes.ma
[260]7Maybe.ma Bool.ma Plogic/equality.ma Universes.ma
8Either.ma Bool.ma Maybe.ma Universes.ma
[352]9DoTest.ma Test.ma
[264]10ASM.ma BitVectorTrie.ma Either.ma String.ma
[316]11Fetch.ma ASM.ma Arithmetic.ma BitVectorTrie.ma
[281]12Char.ma Universes.ma
[352]13Test.ma Assembly.ma Interpret.ma
[344]14Vector.ma Cartesian.ma List.ma Maybe.ma Nat.ma Plogic/equality.ma Util.ma
[260]15Connectives.ma Plogic/equality.ma
16Bool.ma Universes.ma
[264]17Assembly.ma ASM.ma
[329]18List.ma Bool.ma Maybe.ma Nat.ma Plogic/equality.ma Universes.ma Util.ma
[344]19Interpret.ma Arithmetic.ma Cartesian.ma Fetch.ma List.ma Status.ma
[341]20Util.ma Nat.ma
[344]21Compare.ma Universes.ma
[341]22BitVector.ma Bool.ma List.ma Nat.ma Universes.ma Vector.ma
[316]23String.ma Char.ma List.ma
[260]24Plogic/equality.ma Universes.ma
25Nat.ma Bool.ma Cartesian.ma Connectives.ma
Note: See TracBrowser for help on using the repository browser.