_CoqProject 2.13 KB
Newer Older
1
-Q theories iris_time
2 3 4 5 6 7 8 9 10
-arg -w -arg -notation-overridden,-redundant-canonical-projection

theories/heap_lang/lang.v
theories/heap_lang/adequacy.v
theories/heap_lang/lifting.v
theories/heap_lang/notation.v
theories/heap_lang/proofmode.v
theories/heap_lang/tactics.v
theories/heap_lang/lib/assert.v
11

12 13 14 15 16 17 18 19 20 21 22 23
theories/Auth_mnat.v
theories/Auth_nat.v
theories/ClockIntegers.v
theories/Examples.v
theories/Misc.v
theories/Reduction.v
theories/Tactics.v
theories/Simulation.v
theories/Thunks.v
theories/TimeCredits.v
theories/TimeCreditsAltProofs.v
theories/TimeReceipts.v
Glen Mével's avatar
Glen Mével committed
24
theories/Combined.v
25
theories/Translation.v
26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59

theories/union_find/math/Ackermann.v
theories/union_find/math/FilterTowardsInfinity.v
theories/union_find/math/Filter.v
theories/union_find/math/InverseAckermann.v
theories/union_find/math/InverseNatNat.v
theories/union_find/math/LibFunOrd.v
theories/union_find/math/LibIter.v
theories/union_find/math/LibNatExtra.v
theories/union_find/math/LibRewrite.v
theories/union_find/math/MiscArith.v
theories/union_find/math/TLCBuffer.v
theories/union_find/math/UnionFind01Data.v
theories/union_find/math/UnionFind02EmptyCreate.v
theories/union_find/math/UnionFind03Link.v
theories/union_find/math/UnionFind04Compress.v
theories/union_find/math/UnionFind05IteratedCompression.v
theories/union_find/math/UnionFind06Join.v
theories/union_find/math/UnionFind11Rank.v
theories/union_find/math/UnionFind12RankEmptyCreate.v
theories/union_find/math/UnionFind13RankLink.v
theories/union_find/math/UnionFind14RankCompress.v
theories/union_find/math/UnionFind15RankJoin.v
theories/union_find/math/UnionFind21Parent.v
theories/union_find/math/UnionFind22ParentEvolution.v
theories/union_find/math/UnionFind23Evolution.v
theories/union_find/math/UnionFind24Pleasant.v
theories/union_find/math/UnionFind31Potential.v
theories/union_find/math/UnionFind32PotentialCompress.v
theories/union_find/math/UnionFind33PotentialAnalysis.v
theories/union_find/math/UnionFind41Potential.v
theories/union_find/math/UnionFind42PotentialCompress.v
theories/union_find/math/UnionFind43PotentialAnalysis.v
theories/union_find/math/UnionFind44PotentialJoin.v
60
theories/union_find/Code.v
61
theories/union_find/Proof.v