package info (click to toggle)
coq 8.20.1%2Bdfsg-1
  • links: PTS, VCS
  • area: main
  • in suites: forky, sid, trixie
  • size: 44,116 kB
  • sloc: ml: 234,160; sh: 4,301; python: 3,270; ansic: 2,644; makefile: 882; lisp: 172; javascript: 63; xml: 24; sed: 2

Folder: failure

d .. (parent)
- - rw-r--r-- 61 Case1.v
- - rw-r--r-- 116 Case10.v
- - rw-r--r-- 118 Case11.v
- - rw-r--r-- 142 Case12.v
- - rw-r--r-- 145 Case13.v
- - rw-r--r-- 204 Case14.v
- - rw-r--r-- 155 Case15.v
- - rw-r--r-- 199 Case16.v
- - rw-r--r-- 267 Case2.v
- - rw-r--r-- 194 Case3.v
- - rw-r--r-- 141 Case4.v
- - rw-r--r-- 164 Case5.v
- - rw-r--r-- 192 Case6.v
- - rw-r--r-- 456 Case7.v
- - rw-r--r-- 178 Case8.v
- - rw-r--r-- 221 Case9.v
- - rw-r--r-- 246 ClearBody.v
- - rw-r--r-- 126 ImportedCoercion.v
- - rw-r--r-- 148 Notations.v
- - rw-r--r-- 595 PrimitiveProjectionsAttribute_Inductives.v
- - rw-r--r-- 189 Reordering.v
- - rw-r--r-- 58 Sections.v
- - rw-r--r-- 1,080 Tauto.v
- - rw-r--r-- 530 Uminus.v
- - rw-r--r-- 408 autorewritein.v
- - rw-r--r-- 155 cases.v
- - rw-r--r-- 45 check.v
- - rw-r--r-- 299 circular_subtyping.v
- - rw-r--r-- 810 clash_cons.v
- - rw-r--r-- 210 clashes.v
- - rw-r--r-- 393 cofixpoint.v
- - rw-r--r-- 129 evar1.v
- - rw-r--r-- 250 evarclear1.v
- - rw-r--r-- 217 evarclear2.v
- - rw-r--r-- 93 evarlemma.v
- - rw-r--r-- 1,297 extraction_ffi.v
- - rw-r--r-- 778 fixpoint1.v
- - rw-r--r-- 104 fixpoint2.v
- - rw-r--r-- 335 fixpoint3.v
- - rw-r--r-- 557 fixpoint4.v
- - rw-r--r-- 1,969 fixpointeta.v
- - rw-r--r-- 1,015 guard.v
- - rw-r--r-- 1,165 guard_cofix.v
- - rw-r--r-- 693 illtype1.v
- - rw-r--r-- 1,037 inductive.v
- - rw-r--r-- 180 ltac1.v
- - rw-r--r-- 164 ltac2.v
- - rw-r--r-- 158 ltac4.v
- - rw-r--r-- 210 pattern.v
- - rw-r--r-- 1,585 positivity.v
- - rw-r--r-- 405 proofirrelevance.v
- - rw-r--r-- 327 prop_set_proof_irrelevance.v
- - rw-r--r-- 728 redef.v
- - rw-r--r-- 111 rewrite_in_goal.v
- - rw-r--r-- 127 rewrite_in_hyp.v
- - rw-r--r-- 333 rewrite_in_hyp2.v
- - rw-r--r-- 725 search.v
- - rw-r--r-- 4,162 sortelim.v
- - rw-r--r-- 1,050 subterm.v
- - rw-r--r-- 1,249 subterm2.v
- - rw-r--r-- 824 subterm3.v
- - rw-r--r-- 332 subtyping.v
- - rw-r--r-- 6,431 subtyping2.v
- - rw-r--r-- 322 uint63.v
- - rw-r--r-- 564 uip_loop.v
- - rw-r--r-- 534 univ_include.v
- - rw-r--r-- 108 universes.v
- - rw-r--r-- 1,188 universes3.v
- - rw-r--r-- 6,296 universes_buraliforti.v
- - rw-r--r-- 6,844 universes_buraliforti_redef.v
- - rw-r--r-- 205 universes_sections1.v
- - rw-r--r-- 223 universes_sections2.v