package info (click to toggle)
coq 8.16.1%2Bdfsg-1
  • links: PTS, VCS
  • area: main
  • in suites: bookworm
  • size: 40,596 kB
  • sloc: ml: 219,376; sh: 3,545; python: 3,231; ansic: 2,529; makefile: 767; lisp: 279; javascript: 63; xml: 24; sed: 2

Folder: output

d .. (parent)
d d rwxr-xr-x 69 load
- - rw-r--r-- 4,471 Arguments.out
- - rw-r--r-- 1,996 Arguments.v
- - rw-r--r-- 1,695 ArgumentsScope.out
- - rw-r--r-- 607 ArgumentsScope.v
- - rw-r--r-- 4,594 Arguments_renaming.out
- - rw-r--r-- 1,190 Arguments_renaming.v
- - rw-r--r-- 1,095 BadOptionValueType.out
- - rw-r--r-- 183 BadOptionValueType.v
- - rw-r--r-- 206 Binder.out
- - rw-r--r-- 134 Binder.v
- - rw-r--r-- 8,580 Cases.out
- - rw-r--r-- 8,938 Cases.v
- - rw-r--r-- 284 CoercionOnHole.out
- - rw-r--r-- 482 CoercionOnHole.v
- - rw-r--r-- 108 Coercions.out
- - rw-r--r-- 651 Coercions.v
- - rw-r--r-- 139 CompactContexts.out
- - rw-r--r-- 141 CompactContexts.v
- - rw-r--r-- 206 DebugFlags.out
- - rw-r--r-- 72 DebugFlags.v
- - rw-r--r-- 408 DependentInductionErrors.out
- - rw-r--r-- 379 DependentInductionErrors.v
- - rw-r--r-- 150 Deprecation.out
- - rw-r--r-- 102 Deprecation.v
- - rw-r--r-- 0 Emacs_and_diffs.out
- - rw-r--r-- 100 Emacs_and_diffs.v
- - rw-r--r-- 648 EmptyExtraction.out
- - rw-r--r-- 1,016 EmptyExtraction.v
- - rw-r--r-- 167 EqNotation.out
- - rw-r--r-- 83 EqNotation.v
- - rw-r--r-- 414 ErrorInCanonicalStructures.out
- - rw-r--r-- 144 ErrorInCanonicalStructures.v
- - rw-r--r-- 171 ErrorInModule.out
- - rw-r--r-- 104 ErrorInModule.v
- - rw-r--r-- 172 ErrorInSection.out
- - rw-r--r-- 105 ErrorInSection.v
- - rw-r--r-- 292 ErrorLocation_12152.out
- - rw-r--r-- 84 ErrorLocation_12152.v
- - rw-r--r-- 193 ErrorLocation_12255.out
- - rw-r--r-- 125 ErrorLocation_12255.v
- - rw-r--r-- 503 ErrorLocation_12774.out
- - rw-r--r-- 105 ErrorLocation_12774.v
- - rw-r--r-- 291 ErrorLocation_13241.out
- - rw-r--r-- 174 ErrorLocation_13241.v
- - rw-r--r-- 538 ErrorLocation_ltac.out
- - rw-r--r-- 139 ErrorLocation_ltac.v
- - rw-r--r-- 1,113 ErrorLocation_tac_in_term.out
- - rw-r--r-- 352 ErrorLocation_tac_in_term.v
- - rw-r--r-- 691 ErrorModuleWith.out
- - rw-r--r-- 559 ErrorModuleWith.v
- - rw-r--r-- 681 Error_msg_diffs.out
- - rw-r--r-- 909 Error_msg_diffs.v
- - rw-r--r-- 1,795 Errors.out
- - rw-r--r-- 993 Errors.v
- - rw-r--r-- 245 Existentials.out
- - rw-r--r-- 242 Existentials.v
- - rw-r--r-- 59 ExistingInstance.out
- - rw-r--r-- 94 ExistingInstance.v
- - rw-r--r-- 2,638 ExtractionString.out
- - rw-r--r-- 599 ExtractionString.v
- - rw-r--r-- 1,807 Extraction_Haskell_String_12258.out
- - rw-r--r-- 1,854 Extraction_Haskell_String_12258.v
- - rw-r--r-- 279 Extraction_infix.out
- - rw-r--r-- 623 Extraction_infix.v
- - rw-r--r-- 1,058 Extraction_matchs_2413.out
- - rw-r--r-- 2,778 Extraction_matchs_2413.v
- - rw-r--r-- 1,562 Fixpoint.out
- - rw-r--r-- 2,154 Fixpoint.v
- - rw-r--r-- 2,526 FloatExtraction.out
- - rw-r--r-- 1,363 FloatExtraction.v
- - rw-r--r-- 2,251 FloatNumberSyntax.out
- - rw-r--r-- 954 FloatNumberSyntax.v
- - rw-r--r-- 846 FunExt.out
- - rw-r--r-- 4,819 FunExt.v
- - rw-r--r-- 0 Function.out
- - rw-r--r-- 993 Function.v
- - rw-r--r-- 2,997 HintLocality.out
- - rw-r--r-- 2,042 HintLocality.v
- - rw-r--r-- 680 Implicit.out
- - rw-r--r-- 1,852 Implicit.v
- - rw-r--r-- 615 ImplicitTypes.out
- - rw-r--r-- 1,059 ImplicitTypes.v
- - rw-r--r-- 698 Inductive.out
- - rw-r--r-- 535 Inductive.v
- - rw-r--r-- 412 InductiveMainName.out
- - rw-r--r-- 156 InductiveMainName.v
- - rw-r--r-- 312 InitSyntax.out
- - rw-r--r-- 111 InitSyntax.v
- - rw-r--r-- 316 Int31NumberSyntax.out
- - rw-r--r-- 453 Int31NumberSyntax.v
- - rw-r--r-- 1,915 Int63NumberSyntax.out
- - rw-r--r-- 1,142 Int63NumberSyntax.v
- - rw-r--r-- 82 Intuition.out
- - rw-r--r-- 121 Intuition.v
- - rw-r--r-- 1,253 InvalidDisjunctiveIntro.out
- - rw-r--r-- 888 InvalidDisjunctiveIntro.v
- - rw-r--r-- 178 Load.out
- - rw-r--r-- 130 Load.v
- - rw-r--r-- 2,847 MExtraction.v
- - rw-r--r-- 36 Match_subterm.out
- - rw-r--r-- 93 Match_subterm.v
- - rw-r--r-- 1,028 NNumberSyntax.out
- - rw-r--r-- 1,072 NNumberSyntax.v
- - rw-r--r-- 1,790 Nametab.out
- - rw-r--r-- 989 Nametab.v
- - rw-r--r-- 2,440 Naming.out
- - rw-r--r-- 2,688 Naming.v
- - rw-r--r-- 1,095 NatSyntax.out
- - rw-r--r-- 296 NatSyntax.v
- - rw-r--r-- 32 NoAxiomFromR.out
- - rw-r--r-- 186 NoAxiomFromR.v
- - rw-r--r-- 972 NotationSyntax.out
- - rw-r--r-- 357 NotationSyntax.v
- - rw-r--r-- 6,170 Notations.out
- - rw-r--r-- 11,897 Notations.v
- - rw-r--r-- 1,993 Notations2.out
- - rw-r--r-- 4,923 Notations2.v
- - rw-r--r-- 7,998 Notations3.out
- - rw-r--r-- 15,457 Notations3.v
- - rw-r--r-- 7,880 Notations4.out
- - rw-r--r-- 15,014 Notations4.v
- - rw-r--r-- 7,631 Notations5.out
- - rw-r--r-- 7,986 Notations5.v
- - rw-r--r-- 258 NotationsCoercions.out
- - rw-r--r-- 2,064 NotationsCoercions.v
- - rw-r--r-- 799 NotationsSigma.out
- - rw-r--r-- 601 NotationsSigma.v
- - rw-r--r-- 15,457 NumberNotations.out
- - rw-r--r-- 30,380 NumberNotations.v
- - rw-r--r-- 360 Partac.out
- - rw-r--r-- 86 Partac.v
- - rw-r--r-- 1,380 PatternsInBinders.out
- - rw-r--r-- 1,795 PatternsInBinders.v
- - rw-r--r-- 2,813 PosSyntax.out
- - rw-r--r-- 1,568 PosSyntax.v
- - rw-r--r-- 1,084 PrimitiveProjectionsAttribute.out
- - rw-r--r-- 627 PrimitiveProjectionsAttribute.v
- - rw-r--r-- 459 PrimitiveProjectionsAttribute_Records.out
- - rw-r--r-- 390 PrimitiveProjectionsAttribute_Records.v
- - rw-r--r-- 720 PrintAssumptions.out
- - rw-r--r-- 4,481 PrintAssumptions.v
- - rw-r--r-- 560 PrintCanonicalProjections.out
- - rw-r--r-- 1,363 PrintCanonicalProjections.v
- - rw-r--r-- 2,127 PrintGrammarConstr.out
- - rw-r--r-- 152 PrintGrammarConstr.v
- - rw-r--r-- 2,627 PrintInfos.out
- - rw-r--r-- 988 PrintInfos.v
- - rw-r--r-- 356 PrintModule.out
- - rw-r--r-- 834 PrintModule.v
- - rw-r--r-- 16,145 PrintNotation.out
- - rw-r--r-- 6,010 PrintNotation.v
- - rw-r--r-- 23 PrintUnivsSubgraph.out
- - rw-r--r-- 200 PrintUnivsSubgraph.v
- - rw-r--r-- 1,429 PrintingParentheses.out
- - rw-r--r-- 147 PrintingParentheses.v
- - rw-r--r-- 514 Projections.out
- - rw-r--r-- 395 Projections.v
- - rw-r--r-- 1,140 ProofUsingClashWarning.out
- - rw-r--r-- 446 ProofUsingClashWarning.v
- - rw-r--r-- 822 QArithSyntax.out
- - rw-r--r-- 743 QArithSyntax.v
- - rw-r--r-- 861 RealNumberSyntax.out
- - rw-r--r-- 1,129 RealNumberSyntax.v
- - rw-r--r-- 0 RecognizePluginWarning.out
- - rw-r--r-- 280 RecognizePluginWarning.v
- - rw-r--r-- 1,940 Record.out
- - rw-r--r-- 2,255 Record.v
- - rw-r--r-- 997 RecordFieldErrors.out
- - rw-r--r-- 949 RecordFieldErrors.v
- - rw-r--r-- 755 RecordMissingField.out
- - rw-r--r-- 470 RecordMissingField.v
- - rw-r--r-- 900 RecordProjParameter.out
- - rw-r--r-- 329 RecordProjParameter.v
- - rw-r--r-- 17,139 SchemeNames.out
- - rw-r--r-- 7,031 SchemeNames.v
- - rw-r--r-- 20,514 Search.out
- - rw-r--r-- 2,460 Search.v
- - rw-r--r-- 3,450 SearchPattern.out
- - rw-r--r-- 1,003 SearchPattern.v
- - rw-r--r-- 120 SearchRewrite.out
- - rw-r--r-- 384 SearchRewrite.v
- - rw-r--r-- 29 Search_bug13298.out
- - rw-r--r-- 94 Search_bug13298.v
- - rw-r--r-- 2,027 Search_headconcl.out
- - rw-r--r-- 494 Search_headconcl.v
- - rw-r--r-- 139 Show.out
- - rw-r--r-- 265 Show.v
- - rw-r--r-- 58 ShowMatch.out
- - rw-r--r-- 356 ShowMatch.v
- - rw-r--r-- 31 ShowProof.out
- - rw-r--r-- 152 ShowProof.v
- - rw-r--r-- 459 ShowUnivs.out
- - rw-r--r-- 726 ShowUnivs.v
- - rw-r--r-- 1,804 Sint63NumberSyntax.out
- - rw-r--r-- 948 Sint63NumberSyntax.v
- - rw-r--r-- 35,429 StringSyntax.out
- - rw-r--r-- 2,423 StringSyntax.v
- - rw-r--r-- 303 StringSyntaxPrimitive.out
- - rw-r--r-- 4,687 StringSyntaxPrimitive.v
- - rw-r--r-- 395 Succeed.out
- - rw-r--r-- 93 Succeed.v
- - rw-r--r-- 353 SuggestProofUsing.out
- - rw-r--r-- 1,135 SuggestProofUsing.v
- - rw-r--r-- 99 Sum.out
- - rw-r--r-- 93 Sum.v
- - rw-r--r-- 733 Tactics.out
- - rw-r--r-- 1,123 Tactics.v
- - rw-r--r-- 89 TranspModtype.out
- - rw-r--r-- 385 TranspModtype.v
- - rw-r--r-- 841 TypeclassDebug.out
- - rw-r--r-- 244 TypeclassDebug.v
- - rw-r--r-- 158 UnboundRef.out
- - rw-r--r-- 83 UnboundRef.v
- - rw-r--r-- 100 UnclosedBlocks.out
- - rw-r--r-- 182 UnclosedBlocks.v
- - rw-r--r-- 253 UnexpectedType.out
- - rw-r--r-- 997 UnexpectedType.v
- - rw-r--r-- 1,398 Unicode.out
- - rw-r--r-- 981 Unicode.v
- - rw-r--r-- 6,719 UnivBinders.out
- - rw-r--r-- 5,184 UnivBinders.v
- - rw-r--r-- 338 UpdateLoc.out
- - rw-r--r-- 190 UpdateLoc.v
- - rw-r--r-- 14 UsePluginWarning.out
- - rw-r--r-- 131 UsePluginWarning.v
- - rw-r--r-- 13 UselessSyndef.out
- - rw-r--r-- 122 UselessSyndef.v
- - rw-r--r-- 144 Utf8Impargs.out
- - rw-r--r-- 252 Utf8Impargs.v
- - rw-r--r-- 206 Warnings.out
- - rw-r--r-- 187 Warnings.v
- - rw-r--r-- 1,711 ZNumberSyntax.out
- - rw-r--r-- 1,808 ZNumberSyntax.v
- - rw-r--r-- 263 allBytes.out
- - rw-r--r-- 5,063 allBytes.v
- - rw-r--r-- 488 auto.out
- - rw-r--r-- 171 auto.v
- - rw-r--r-- 381 bug12442.out
- - rw-r--r-- 162 bug12442.v
- - rw-r--r-- 290 bug5778.out
- - rw-r--r-- 144 bug5778.v
- - rw-r--r-- 300 bug6404.out
- - rw-r--r-- 156 bug6404.v
- - rw-r--r-- 59 bug6821.out
- - rw-r--r-- 258 bug6821.v
- - rw-r--r-- 96 bug7191.out
- - rw-r--r-- 105 bug7191.v
- - rw-r--r-- 650 bug7348.out
- - rw-r--r-- 513 bug7348.v
- - rw-r--r-- 86 bug_10803.out
- - rw-r--r-- 415 bug_10803.v
- - rw-r--r-- 30 bug_10824.out
- - rw-r--r-- 220 bug_10824.v
- - rw-r--r-- 14 bug_11342.out
- - rw-r--r-- 316 bug_11342.v
- - rw-r--r-- 28 bug_11608.out
- - rw-r--r-- 340 bug_11608.v
- - rw-r--r-- 226 bug_11934.out
- - rw-r--r-- 443 bug_11934.v
- - rw-r--r-- 210 bug_12159.out
- - rw-r--r-- 855 bug_12159.v
- - rw-r--r-- 19 bug_12777.out
- - rw-r--r-- 84 bug_12777.v
- - rw-r--r-- 440 bug_12887.out
- - rw-r--r-- 251 bug_12887.v
- - rw-r--r-- 264 bug_12908.out
- - rw-r--r-- 354 bug_12908.v
- - rw-r--r-- 61 bug_13004.out
- - rw-r--r-- 125 bug_13004.v
- - rw-r--r-- 240 bug_13018.out
- - rw-r--r-- 1,363 bug_13018.v
- - rw-r--r-- 31 bug_13112.out
- - rw-r--r-- 169 bug_13112.v
- - rw-r--r-- 106 bug_13238.out
- - rw-r--r-- 176 bug_13238.v
- - rw-r--r-- 73 bug_13240.out
- - rw-r--r-- 133 bug_13240.v
- - rw-r--r-- 522 bug_13244.out
- - rw-r--r-- 87 bug_13244.v
- - rw-r--r-- 496 bug_13266.out
- - rw-r--r-- 252 bug_13266.v
- - rw-r--r-- 123 bug_13320.out
- - rw-r--r-- 87 bug_13320.v
- - rw-r--r-- 282 bug_13595.out
- - rw-r--r-- 247 bug_13595.v
- - rw-r--r-- 0 bug_13821_native_command_line_warn.out
- - rw-r--r-- 158 bug_13821_native_command_line_warn.v
- - rw-r--r-- 414 bug_13857.out
- - rw-r--r-- 182 bug_13857.v
- - rw-r--r-- 4,120 bug_13942.out
- - rw-r--r-- 11,417 bug_13942.v
- - rw-r--r-- 203 bug_14815.out
- - rw-r--r-- 113 bug_14815.v
- - rw-r--r-- 94 bug_14899.out
- - rw-r--r-- 103 bug_14899.v
- - rw-r--r-- 348 bug_15097.out
- - rw-r--r-- 85 bug_15097.v
- - rw-r--r-- 127 bug_15106.out
- - rw-r--r-- 214 bug_15106.v
- - rw-r--r-- 151 bug_15334.out
- - rw-r--r-- 147 bug_15334.v
- - rw-r--r-- 35 bug_15709.out
- - rw-r--r-- 88 bug_15709.v
- - rw-r--r-- 51 bug_16411.out
- - rw-r--r-- 158 bug_16411.v
- - rw-r--r-- 154 bug_16613.out
- - rw-r--r-- 72 bug_16613.v
- - rw-r--r-- 153 bug_3810.out
- - rw-r--r-- 217 bug_3810.v
- - rw-r--r-- 54 bug_4167.out
- - rw-r--r-- 164 bug_4167.v
- - rw-r--r-- 235 bug_4337.out
- - rw-r--r-- 111 bug_4337.v
- - rw-r--r-- 282 bug_5222.out
- - rw-r--r-- 433 bug_5222.v
- - rw-r--r-- 152 bug_6764.out
- - rw-r--r-- 601 bug_6764.v
- - rw-r--r-- 283 bug_7443.out
- - rw-r--r-- 1,698 bug_7443.v
- - rw-r--r-- 307 bug_8206.out
- - rw-r--r-- 268 bug_8206.v
- - rw-r--r-- 103 bug_9180.out
- - rw-r--r-- 296 bug_9180.v
- - rw-r--r-- 147 bug_9370.out
- - rw-r--r-- 159 bug_9370.v
- - rw-r--r-- 154 bug_9403.out
- - rw-r--r-- 3,401 bug_9403.v
- - rw-r--r-- 74 bug_9555.out
- - rw-r--r-- 100 bug_9555.v
- - rw-r--r-- 362 bug_9569.out
- - rw-r--r-- 546 bug_9569.v
- - rw-r--r-- 112 bug_9682.out
- - rw-r--r-- 1,381 bug_9682.v
- - rw-r--r-- 63 clear.out
- - rw-r--r-- 241 clear.v
- - rw-r--r-- 98 coercions_cs.out
- - rw-r--r-- 541 coercions_cs.v
- - rw-r--r-- 528 coercions_nonuniform.out
- - rw-r--r-- 1,547 coercions_nonuniform.v
- - rw-r--r-- 182 coercions_tc.out
- - rw-r--r-- 680 coercions_tc.v
- - rw-r--r-- 1,233 deprecation_definition.out
- - rw-r--r-- 365 deprecation_definition.v
- - rw-r--r-- 197 detype_cast.out
- - rw-r--r-- 115 detype_cast.v
- - rw-r--r-- 270 extra_dep.out
- - rw-r--r-- 106 extra_dep.v
- - rw-r--r-- 1,087 goal_output.out
- - rw-r--r-- 573 goal_output.v
- - rw-r--r-- 85 idtac.out
- - rw-r--r-- 997 idtac.v
- - rw-r--r-- 453 inference.out
- - rw-r--r-- 734 inference.v
- - rw-r--r-- 248 injection.out
- - rw-r--r-- 211 injection.v
- - rw-r--r-- 154 interleave_options_bad_order.out
- - rw-r--r-- 100 interleave_options_bad_order.v
- - rw-r--r-- 27 interleave_options_correct_order.out
- - rw-r--r-- 100 interleave_options_correct_order.v
- - rw-r--r-- 610 locate.out
- - rw-r--r-- 464 locate.v
- - rw-r--r-- 2,072 ltac.out
- - rw-r--r-- 1,732 ltac.v
- - rw-r--r-- 537 ltac2_deprecated.out
- - rw-r--r-- 339 ltac2_deprecated.v
- - rw-r--r-- 647 ltac2_notations_eval_in.out
- - rw-r--r-- 1,065 ltac2_notations_eval_in.v
- - rw-r--r-- 618 ltac_extra_args.out
- - rw-r--r-- 135 ltac_extra_args.v
- - rw-r--r-- 2,415 ltac_missing_args.out
- - rw-r--r-- 405 ltac_missing_args.v
- - rw-r--r-- 323 names.out
- - rw-r--r-- 235 names.v
- - rw-r--r-- 1,363 notation_principal_scope.out
- - rw-r--r-- 629 notation_principal_scope.v
- - rw-r--r-- 18 onlyprinting.out
- - rw-r--r-- 107 onlyprinting.v
- - rw-r--r-- 96 optimize_heap.out
- - rw-r--r-- 115 optimize_heap.v
- - rw-r--r-- 242 prim_array.out
- - rw-r--r-- 153 prim_array.v
- - rw-r--r-- 1,397 primitive_tokens.out
- - rw-r--r-- 459 primitive_tokens.v
- - rw-r--r-- 3,416 print_ltac.out
- - rw-r--r-- 2,350 print_ltac.v
- - rw-r--r-- 257 qualification.out
- - rw-r--r-- 370 qualification.v
- - rw-r--r-- 44 reduction.out
- - rw-r--r-- 279 reduction.v
- - rw-r--r-- 2,798 relaxed_ambiguous_paths.out
- - rw-r--r-- 3,768 relaxed_ambiguous_paths.v
- - rw-r--r-- 149 rewrite_2172.out
- - rw-r--r-- 741 rewrite_2172.v
- - rw-r--r-- 112 section_have.out
- - rw-r--r-- 169 section_have.v
- - rw-r--r-- 267 set.out
- - rw-r--r-- 154 set.v
- - rw-r--r-- 0 signatureT.out
- - rw-r--r-- 43 signatureT.v
- - rw-r--r-- 189 simpl.out
- - rw-r--r-- 155 simpl.v
- - rw-r--r-- 374 sint63NumberNotation.out
- - rw-r--r-- 1,023 sint63NumberNotation.v
- - rw-r--r-- 134 ssr_clear.out
- - rw-r--r-- 97 ssr_clear.v
- - rw-r--r-- 139 ssr_error_multiple_intro_after_case.out
- - rw-r--r-- 85 ssr_error_multiple_intro_after_case.v
- - rw-r--r-- 2,436 ssr_explain_match.out
- - rw-r--r-- 1,033 ssr_explain_match.v
- - rw-r--r-- 135 ssr_pred.out
- - rw-r--r-- 55 ssr_pred.v
- - rw-r--r-- 126 ssr_under.out
- - rw-r--r-- 806 ssr_under.v
- - rw-r--r-- 613 subst.out
- - rw-r--r-- 836 subst.v
- - rw-r--r-- 1,015 undeclared_key.out
- - rw-r--r-- 206 undeclared_key.v
- - rw-r--r-- 1,756 unifconstraints.out
- - rw-r--r-- 907 unifconstraints.v
- - rw-r--r-- 1,082 unification.out
- - rw-r--r-- 839 unification.v