package info (click to toggle)
coq 8.2.pl2%2Bdfsg-1
  • links: PTS, VCS
  • area: main
  • in suites: squeeze
  • size: 17,644 kB
  • ctags: 22,672
  • sloc: ml: 133,155; ansic: 1,960; sh: 1,372; lisp: 456; makefile: 363

Folder: success

d .. (parent)
- - rw-r--r-- 446 Abstract.v
- - rw-r--r-- 2,979 AdvancedCanonicalStructure.v
- - rw-r--r-- 713 CanonicalStructure.v
- - rw-r--r-- 335 Case1.v
- - rw-r--r-- 738 Case10.v
- - rw-r--r-- 341 Case11.v
- - rw-r--r-- 2,074 Case12.v
- - rw-r--r-- 2,149 Case13.v
- - rw-r--r-- 510 Case14.v
- - rw-r--r-- 1,318 Case15.v
- - rw-r--r-- 405 Case16.v
- - rw-r--r-- 1,850 Case17.v
- - rw-r--r-- 513 Case18.v
- - rw-r--r-- 272 Case19.v
- - rw-r--r-- 306 Case2.v
- - rw-r--r-- 365 Case5.v
- - rw-r--r-- 583 Case6.v
- - rw-r--r-- 474 Case7.v
- - rw-r--r-- 338 Case8.v
- - rw-r--r-- 2,237 Case9.v
- - rw-r--r-- 386 CaseAlias.v
- - rw-r--r-- 379 Cases-bug1834.v
- - rw-r--r-- 38,268 Cases.v
- - rw-r--r-- 12,108 CasesDep.v
- - rw-r--r-- 795 Check.v
- - rw-r--r-- 231 Conjecture.v
- - rw-r--r-- 1 DHyp.v
- - rw-r--r-- 218 Decompose.v
- - rw-r--r-- 435 DiscrR.v
- - rw-r--r-- 571 Discriminate.v
- - rw-r--r-- 10,700 Equations.v
- - rw-r--r-- 1,906 Field.v
- - rw-r--r-- 1,400 Fixpoint.v
- - rw-r--r-- 283 Fourier.v
- - rw-r--r-- 10,176 Funind.v
- - rw-r--r-- 253 Generalization.v
- - rw-r--r-- 176 Generalize.v
- - rw-r--r-- 1,261 Hints.v
- - rw-r--r-- 545 ImplicitArguments.v
- - rw-r--r-- 549 ImplicitTactic.v
- - rw-r--r-- 1,427 Inductive.v
- - rw-r--r-- 1,769 Injection.v
- - rw-r--r-- 2,859 Inversion.v
- - rw-r--r-- 1,768 LegacyField.v
- - rw-r--r-- 356 LetIn.v
- - rw-r--r-- 1,756 LetPat.v
- - rw-r--r-- 822 MatchFail.v
- - rw-r--r-- 302 Mod_ltac.v
- - rw-r--r-- 1,445 Mod_params.v
- - rw-r--r-- 963 Mod_strengthen.v
- - rw-r--r-- 269 Mod_type.v
- - rw-r--r-- 125 NatRing.v
- - rw-r--r-- 1,077 Notations.v
- - rw-r--r-- 2,197 Omega.v
- - rw-r--r-- 2,449 Omega0.v
- - rw-r--r-- 764 Omega2.v
- - rw-r--r-- 2,183 OmegaPre.v
- - rw-r--r-- 207 PPFix.v
- - rw-r--r-- 282 Print.v
- - rw-r--r-- 1,154 Projection.v
- - rw-r--r-- 2,243 ROmega.v
- - rw-r--r-- 2,564 ROmega0.v
- - rw-r--r-- 984 ROmega2.v
- - rw-r--r-- 2,204 ROmegaPre.v
- - rw-r--r-- 25,255 RecTutorial.v
- - rw-r--r-- 2,253 Record.v
- - rw-r--r-- 3,094 Reg.v
- - rw-r--r-- 172 Remark.v
- - rw-r--r-- 220 Rename.v
- - rw-r--r-- 378 Reordering.v
- - rw-r--r-- 88 Require.v
- - rw-r--r-- 77 Reset.v
- - rw-r--r-- 157 Scopes.v
- - rw-r--r-- 258 Simplify_eq.v
- - rw-r--r-- 5,202 Tauto.v
- - rw-r--r-- 4,406 TestRefine.v
- - rw-r--r-- 182 Try.v
- - rw-r--r-- 6,323 apply.v
- - rw-r--r-- 521 autorewritein.v
- - rw-r--r-- 2,403 cc.v
- - rw-r--r-- 186 change.v
- - rw-r--r-- 291 clear.v
- - rw-r--r-- 2,133 coercions.v
- - rw-r--r-- 7,485 conv_pbs.v
- - rw-r--r-- 211 coqbugs0181.v
- - rw-r--r-- 5,547 decl_mode.v
- - rw-r--r-- 3,330 dependentind.v
- - rw-r--r-- 1,089 destruct.v
- - rw-r--r-- 1,868 eauto.v
- - rw-r--r-- 912 eqdecide.v
- - rw-r--r-- 6,522 evars.v
- - rw-r--r-- 14,264 extraction.v
- - rw-r--r-- 2,212 fix.v
- - rw-r--r-- 322 guard.v
- - rw-r--r-- 1,153 hyps_inclusion.v
- - rw-r--r-- 366 if.v
- - rw-r--r-- 1,117 implicit.v
- - rw-r--r-- 3,467 import_lib.v
- - rw-r--r-- 993 import_mod.v
- - rw-r--r-- 594 inds_type_sec.v
- - rw-r--r-- 698 induct.v
- - rw-r--r-- 292 instantiate.v
- - rw-r--r-- 168 intros.v
- - rw-r--r-- 4,393 ltac.v
- - rw-r--r-- 1,604 mutual_ind.v
- - rw-r--r-- 690 options.v
- - rw-r--r-- 93 params_ind.v
- - rw-r--r-- 243 parsing.v
- - rw-r--r-- 379 pattern.v
- - rw-r--r-- 220 polymorphism.v
- - rw-r--r-- 2,668 refine.v
- - rw-r--r-- 359 replace.v
- - rw-r--r-- 944 rewrite.v
- - rw-r--r-- 148 rewrite_in.v
- - rw-r--r-- 545 rewrite_iterated.v
- - rw-r--r-- 90 set.v
- - rw-r--r-- 925 setoid_ring_module.v
- - rw-r--r-- 2,657 setoid_test.v
- - rw-r--r-- 8,257 setoid_test2.v
- - rw-r--r-- 1,434 setoid_test_function_space.v
- - rw-r--r-- 1,239 simpl.v
- - rw-r--r-- 1,459 specialize.v
- - rw-r--r-- 644 unfold.v
- - rw-r--r-- 2,172 unicode_utf8.v
- - rw-r--r-- 3,912 unification.v
- - rw-r--r-- 1,752 univers.v