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

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

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

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