aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2020-08-27Merge PR #12913: Modify lia to work with -mangle-namescoqbot-app[bot]
2020-08-27Merge PR #12850: Avoid running configure when plugins/ modifiedcoqbot-app[bot]
2020-08-27Merge PR #12877: Propagate in-context information for explicitation of extra ...coqbot-app[bot]
2020-08-27Merge PR #12867: Fast freeze summarycoqbot-app[bot]
2020-08-27Merge PR #12911: Use the lite variants of performance tests in the bench defa...coqbot-app[bot]
2020-08-27tacinterp mini cleanup useless letinGaëtan Gilbert
2020-08-27Merge PR #12898: [ssr] backport ssrbool from Math Comp 1.11Enrico Tassi
2020-08-26Merge PR #12085: Convert ltac2 chapter to use prodn, update syntaxcoqbot-app[bot]
2020-08-26Modify lia to work with -mangle-namesJasper Hugunin
2020-08-26Wrap future goals into a moduleMaxime Dénès
2020-08-26Add test for #10939Maxime Dénès
2020-08-26Make future_goals stack explicit in the evarmapMaxime Dénès
2020-08-26Move given_up goals to evar_mapMaxime Dénès
2020-08-26Better encapsulation of future goalsMaxime Dénès
2020-08-26Fix algebraic comparison with sprop on one sideGaëtan Gilbert
2020-08-26Use the lite variants of performance tests in the bench default packages.Pierre-Marie Pédrot
2020-08-26Merge PR #12764: A fix and two enhancements of trailing pattern factorization...Pierre-Marie Pédrot
2020-08-26Merge PR #12904: Move bench job definition to its own filePierre-Marie Pédrot
2020-08-26Merge PR #12881: Deprecate intro_usingPierre-Marie Pédrot
2020-08-26Merge PR #12901: [bench] Remove useless commit guessing logicPierre-Marie Pédrot
2020-08-26Merge PR #12884: Documentation of coq_makefile: fix name of installation dir ...coqbot-app[bot]
2020-08-26Merge PR #12861: Require NsatzTactic: nsatz support for Z and QPierre-Marie Pédrot
2020-08-26address comments and fixupsReynald Affeldt
2020-08-25Documentation of coq_makefile: fix name of installation dir + help on option -f.Hugo Herbelin
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