package info
(click to toggle)
Folder: failure
![]() |
.. (parent) | |||
![]() |
- | rw-r--r-- | 56 | Case1.v |
![]() |
- | rw-r--r-- | 111 | Case10.v |
![]() |
- | rw-r--r-- | 113 | Case11.v |
![]() |
- | rw-r--r-- | 137 | Case12.v |
![]() |
- | rw-r--r-- | 140 | Case13.v |
![]() |
- | rw-r--r-- | 199 | Case14.v |
![]() |
- | rw-r--r-- | 150 | Case15.v |
![]() |
- | rw-r--r-- | 194 | Case16.v |
![]() |
- | rw-r--r-- | 262 | Case2.v |
![]() |
- | rw-r--r-- | 189 | Case3.v |
![]() |
- | rw-r--r-- | 136 | Case4.v |
![]() |
- | rw-r--r-- | 159 | Case5.v |
![]() |
- | rw-r--r-- | 187 | Case6.v |
![]() |
- | rw-r--r-- | 451 | Case7.v |
![]() |
- | rw-r--r-- | 173 | Case8.v |
![]() |
- | rw-r--r-- | 224 | Case9.v |
![]() |
- | rw-r--r-- | 234 | ClearBody.v |
![]() |
- | rw-r--r-- | 121 | ImportedCoercion.v |
![]() |
- | rw-r--r-- | 143 | Notations.v |
![]() |
- | rw-r--r-- | 177 | Reordering.v |
![]() |
- | rw-r--r-- | 35 | Sections.v |
![]() |
- | rw-r--r-- | 918 | Tauto.v |
![]() |
- | rw-r--r-- | 1,422 | Uminus.v |
![]() |
- | rw-r--r-- | 388 | autorewritein.v |
![]() |
- | rw-r--r-- | 150 | cases.v |
![]() |
- | rw-r--r-- | 49 | check.v |
![]() |
- | rw-r--r-- | 223 | circular_subtyping1.v |
![]() |
- | rw-r--r-- | 235 | circular_subtyping2.v |
![]() |
- | rw-r--r-- | 655 | clash_cons.v |
![]() |
- | rw-r--r-- | 198 | clashes.v |
![]() |
- | rw-r--r-- | 159 | coqbugs0266.v |
![]() |
- | rw-r--r-- | 124 | evar1.v |
![]() |
- | rw-r--r-- | 239 | evarclear1.v |
![]() |
- | rw-r--r-- | 205 | evarclear2.v |
![]() |
- | rw-r--r-- | 88 | evarlemma.v |
![]() |
- | rw-r--r-- | 619 | fixpoint1.v |
![]() |
- | rw-r--r-- | 92 | fixpoint2.v |
![]() |
- | rw-r--r-- | 330 | fixpoint3.v |
![]() |
- | rw-r--r-- | 552 | fixpoint4.v |
![]() |
- | rw-r--r-- | 856 | guard.v |
![]() |
- | rw-r--r-- | 538 | illtype1.v |
![]() |
- | rw-r--r-- | 179 | inductive1.v |
![]() |
- | rw-r--r-- | 179 | inductive2.v |
![]() |
- | rw-r--r-- | 253 | inductive3.v |
![]() |
- | rw-r--r-- | 521 | inductive4.v |
![]() |
- | rw-r--r-- | 168 | ltac1.v |
![]() |
- | rw-r--r-- | 152 | ltac2.v |
![]() |
- | rw-r--r-- | 147 | ltac4.v |
![]() |
- | rw-r--r-- | 195 | pattern.v |
![]() |
- | rw-r--r-- | 571 | positivity.v |
![]() |
- | rw-r--r-- | 411 | proofirrelevance.v |
![]() |
- | rw-r--r-- | 311 | prop-set-proof-irrelevance.v |
![]() |
- | rw-r--r-- | 573 | redef.v |
![]() |
- | rw-r--r-- | 99 | rewrite_in_goal.v |
![]() |
- | rw-r--r-- | 115 | rewrite_in_hyp.v |
![]() |
- | rw-r--r-- | 321 | rewrite_in_hyp2.v |
![]() |
- | rw-r--r-- | 570 | search.v |
![]() |
- | rw-r--r-- | 251 | subtyping.v |
![]() |
- | rw-r--r-- | 6,425 | subtyping2.v |
![]() |
- | rw-r--r-- | 523 | univ_include.v |
![]() |
- | rw-r--r-- | 6,825 | universes-buraliforti-redef.v |
![]() |
- | rw-r--r-- | 6,291 | universes-buraliforti.v |
![]() |
- | rw-r--r-- | 200 | universes-sections1.v |
![]() |
- | rw-r--r-- | 218 | universes-sections2.v |
![]() |
- | rw-r--r-- | 103 | universes.v |
![]() |
- | rw-r--r-- | 1,183 | universes3.v |