aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2020-08-25Modify Numbers/NatInt/NZGcd.v to compile with -mangle-namesJasper Hugunin
2020-08-25Modify Numbers/NatInt/NZDiv.v to compile with -mangle-namesJasper Hugunin
2020-08-25Modify Numbers/NatInt/NZLog.v to compile with -mangle-namesJasper Hugunin
2020-08-25Modify Numbers/NatInt/NZSqrt.v to compile with -mangle-namesJasper Hugunin
2020-08-25Modify Numbers/NatInt/NZPow.v to compile with -mangle-namesJasper Hugunin
2020-08-25Modify Numbers/NatInt/NZParity.v to compile with -mangle-namesJasper Hugunin
2020-08-25Modify Numbers/NatInt/NZMulOrder.v to compile with -mangle-namesJasper Hugunin
2020-08-25Modify Numbers/NatInt/NZOrder.v to compile with -mangle-namesJasper Hugunin
2020-08-25Modify Numbers/NatInt/NZMul.v to compile with -mangle-namesJasper Hugunin
2020-08-25Modify Numbers/NatInt/NZAdd.v to compile with -mangle-namesJasper Hugunin
2020-08-25Modify Numbers/NatInt/NZBase.v to compile with -mangle-namesJasper Hugunin
2020-08-25Modify Structures/GenericMinMax.v to compile with -mangle-namesJasper Hugunin
2020-08-25Modify Structures/OrdersFacts.v to compile with -mangle-namesJasper Hugunin
2020-08-25Modify Structures/OrdersTac.v to compile with -mangle-namesJasper Hugunin
2020-08-25Modify Structures/Orders.v to compile with -mangle-namesJasper Hugunin
2020-08-25Modify Relations/Relations.v to compile with -mangle-namesJasper Hugunin
2020-08-25Modify Relations/Operators_Properties.v to compile with -mangle-namesJasper Hugunin
2020-08-25Modify Setoids/Setoid.v to compile with -mangle-namesJasper Hugunin
2020-08-25Modify Classes/CMorphisms.v to compile with -mangle-namesJasper Hugunin
2020-08-25Modify Classes/CRelationClasses.v to compile with -mangle-namesJasper Hugunin
2020-08-25Modify Classes/Morphisms.v to compile with -mangle-namesJasper Hugunin
2020-08-25Modify Classes/RelationClasses.v to compile with -mangle-namesJasper Hugunin
2020-08-25Modify Bool/Bool.v to compile with -mangle-namesJasper Hugunin
2020-08-25Modify Init/Tactics.v to compile with -mangle-namesJasper Hugunin
2020-08-25Modify Init/Wf.v to compile with -mangle-namesJasper Hugunin
2020-08-25Modify Init/Peano.v to compile with -mangle-names.Jasper Hugunin
2020-08-25Moving production_level_eq to extend.ml for separation of concerns.Hugo Herbelin
2020-08-25A fix and two enhancements of trailing pattern factorization in rec. notations.Hugo Herbelin
2020-08-25Move bench job definition to its own fileGaëtan Gilbert
2020-08-25Require NsatzTactic: nsatz support for Z and QJason Gross
2020-08-25Remove useless commit guessing logicJason Gross
2020-08-25Convert ltac2 chapter to use prodn, update syntaxJim Fehrle
2020-08-25[bench] Update bench script with better urls and more infoJason Gross
2020-08-25Merge PR #12879: added numeral_notation to META.coq.incoqbot-app[bot]
2020-08-25Merge PR #12897: [test-suite] close the proof added in #12857coqbot-app[bot]
2020-08-25Deprecate intro_usingGaëtan Gilbert
2020-08-25omega: stop using intro_usingGaëtan Gilbert
2020-08-25funind: stop using intro_usingGaëtan Gilbert
2020-08-25elim.ml: stop using intro_usingGaëtan Gilbert
2020-08-25Make decide equality compatible with mangled names.Gaëtan Gilbert
2020-08-25fix notation-incompatible-format warningsReynald Affeldt
2020-08-25The body of a let is considered to be "in context" if its type is present.Hugo Herbelin
2020-08-25Merge PR #12758: Fixing a coercion entry transitivity bug.coqbot-app[bot]
2020-08-25ring: generate fresh names for lemmasGaëtan Gilbert
2020-08-25Merge PR #12801: Put cyclic numbers in sort Set instead of TypeAnton Trunov
2020-08-25[test-suite] close the proofEnrico Tassi
2020-08-25added coq.vernac dependency to string_notations pluginAli Caglayan
2020-08-25Merge PR #12888: Add /dev/bench to CODEOWNERScoqbot-app[bot]
2020-08-25Merge PR #12728: Fix slow Print Universes Subgraph when many ambient universes.coqbot-app[bot]
2020-08-25Propagate in-context information for extra arguments of notations too.Hugo Herbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-06 19:01:59 +0000