coq - The formal proof system

Age	Commit message (Expand)	Author
2020-08-27	tacinterp mini cleanup useless letin	Gaëtan Gilbert
2020-08-27	Merge PR #12898: [ssr] backport ssrbool from Math Comp 1.11	Enrico Tassi
2020-08-26	Merge PR #12085: Convert ltac2 chapter to use prodn, update syntax	coqbot-app[bot]
2020-08-26	Modify lia to work with -mangle-names	Jasper Hugunin
2020-08-26	Wrap future goals into a module	Maxime Dénès
2020-08-26	Add test for #10939	Maxime Dénès
2020-08-26	Make future_goals stack explicit in the evarmap	Maxime Dénès
2020-08-26	Move given_up goals to evar_map	Maxime Dénès
2020-08-26	Better encapsulation of future goals	Maxime Dénès
2020-08-26	Fix algebraic comparison with sprop on one side	Gaëtan Gilbert
2020-08-26	Use the lite variants of performance tests in the bench default packages.	Pierre-Marie Pédrot
2020-08-26	Merge PR #12764: A fix and two enhancements of trailing pattern factorization...	Pierre-Marie Pédrot
2020-08-26	Merge PR #12904: Move bench job definition to its own file	Pierre-Marie Pédrot
2020-08-26	Merge PR #12881: Deprecate intro_using	Pierre-Marie Pédrot
2020-08-26	Merge PR #12901: [bench] Remove useless commit guessing logic	Pierre-Marie Pédrot
2020-08-26	Merge PR #12884: Documentation of coq_makefile: fix name of installation dir ...	coqbot-app[bot]
2020-08-26	Merge PR #12861: Require NsatzTactic: nsatz support for Z and Q	Pierre-Marie Pédrot
2020-08-26	address comments and fixups	Reynald Affeldt
2020-08-25	Documentation of coq_makefile: fix name of installation dir + help on option -f.	Hugo Herbelin
2020-08-25	Modify Numbers/NatInt/NZGcd.v to compile with -mangle-names	Jasper Hugunin
2020-08-25	Modify Numbers/NatInt/NZDiv.v to compile with -mangle-names	Jasper Hugunin
2020-08-25	Modify Numbers/NatInt/NZLog.v to compile with -mangle-names	Jasper Hugunin
2020-08-25	Modify Numbers/NatInt/NZSqrt.v to compile with -mangle-names	Jasper Hugunin
2020-08-25	Modify Numbers/NatInt/NZPow.v to compile with -mangle-names	Jasper Hugunin
2020-08-25	Modify Numbers/NatInt/NZParity.v to compile with -mangle-names	Jasper Hugunin
2020-08-25	Modify Numbers/NatInt/NZMulOrder.v to compile with -mangle-names	Jasper Hugunin
2020-08-25	Modify Numbers/NatInt/NZOrder.v to compile with -mangle-names	Jasper Hugunin
2020-08-25	Modify Numbers/NatInt/NZMul.v to compile with -mangle-names	Jasper Hugunin
2020-08-25	Modify Numbers/NatInt/NZAdd.v to compile with -mangle-names	Jasper Hugunin
2020-08-25	Modify Numbers/NatInt/NZBase.v to compile with -mangle-names	Jasper Hugunin
2020-08-25	Modify Structures/GenericMinMax.v to compile with -mangle-names	Jasper Hugunin
2020-08-25	Modify Structures/OrdersFacts.v to compile with -mangle-names	Jasper Hugunin
2020-08-25	Modify Structures/OrdersTac.v to compile with -mangle-names	Jasper Hugunin
2020-08-25	Modify Structures/Orders.v to compile with -mangle-names	Jasper Hugunin
2020-08-25	Modify Relations/Relations.v to compile with -mangle-names	Jasper Hugunin
2020-08-25	Modify Relations/Operators_Properties.v to compile with -mangle-names	Jasper Hugunin
2020-08-25	Modify Setoids/Setoid.v to compile with -mangle-names	Jasper Hugunin
2020-08-25	Modify Classes/CMorphisms.v to compile with -mangle-names	Jasper Hugunin
2020-08-25	Modify Classes/CRelationClasses.v to compile with -mangle-names	Jasper Hugunin
2020-08-25	Modify Classes/Morphisms.v to compile with -mangle-names	Jasper Hugunin
2020-08-25	Modify Classes/RelationClasses.v to compile with -mangle-names	Jasper Hugunin
2020-08-25	Modify Bool/Bool.v to compile with -mangle-names	Jasper Hugunin
2020-08-25	Modify Init/Tactics.v to compile with -mangle-names	Jasper Hugunin
2020-08-25	Modify Init/Wf.v to compile with -mangle-names	Jasper Hugunin
2020-08-25	Modify Init/Peano.v to compile with -mangle-names.	Jasper Hugunin
2020-08-25	Moving production_level_eq to extend.ml for separation of concerns.	Hugo Herbelin
2020-08-25	A fix and two enhancements of trailing pattern factorization in rec. notations.	Hugo Herbelin
2020-08-25	Move bench job definition to its own file	Gaëtan Gilbert
2020-08-25	Require NsatzTactic: nsatz support for Z and Q	Jason Gross
2020-08-25	Remove useless commit guessing logic	Jason Gross