coq - The formal proof system

Age	Commit message (Expand)	Author
2020-04-01	[micromega] use Coqlib.lib_ref to get Coq constants.	Frédéric Besson
2020-03-31	NArith, PArith: Add facts about iter	Lysxia
2020-03-30	Merge PR #11725: Cleanup stdlib reals.	Hugo Herbelin
2020-03-30	Missing apartness notations	Vincent Semeria
2020-03-30	new sig notations and spaces added	Olivier Laurent
2020-03-30	Merge PR #11018: “auto with zarith”: use “lia” rather than “omega”	Maxime Dénès
2020-03-28	Remove SearchAbout command, deprecated in 8.5	Jim Fehrle
2020-03-27	Cleanup stdlib reals. Use implicit arguments for ConstructiveReals. Move Cons...	Vincent Semeria
2020-03-27	Merge PR #11848: Nicer printing for decimal constants	Hugo Herbelin
2020-03-26	Merge PR #11885: Sorting: Swap the names of Sorted_sort and LocallySorted_sort	Hugo Herbelin
2020-03-25	Make the level of ≡ in Int63 consistent with =	Jason Gross
2020-03-25	Nicer printing for decimal constants in Q	Pierre Roux
2020-03-24	“auto with zarith”: use “lia” rather than “omega”	Vincent Laporte
2020-03-24	[stdlib] Do not rely on failing “auto”	Vincent Laporte
2020-03-23	Fix levels of `<=?` and `<?` in the stdlib	Jason Gross
2020-03-23	Sorting: Swap the names of Sorted_sort and LocallySorted_sort	Lysxia
2020-03-21	Add module ZifyPow to avoid compatibility issue with 8.11.	Théo Zimmermann
2020-03-19	Merge PR #11760: firstorder: default tactic is “auto with core”	Théo Zimmermann
2020-03-19	Merge PR #11822: Grants #11692: clear dependent knows about let-in	Pierre-Marie Pédrot
2020-03-19	firstorder: default tactic is “auto with core”	Vincent Laporte
2020-03-19	[stdlib] Remove a few `auto with *`	Vincent Laporte
2020-03-18	Update headers in the whole code base.	Théo Zimmermann
2020-03-18	Merge PR #11746: Register commonly used names from the Reals library for plug...	Théo Zimmermann
2020-03-14	Fixes #11692 (clear dependent knows about let-in).	Hugo Herbelin
2020-03-06	Fix #11738 : Funind using deprecated Coqlib API.	Pierre Courtieu
2020-03-04	Add file to register names of reals library used by gappa	Michael Soegtrop
2020-03-03	[zify] efficiency improvements	Frédéric Besson
2020-02-26	Merge PR #11644: Use implicit arguments in notations for eq.	Hugo Herbelin
2020-02-26	Consolidate int63-related notations	Maxime Dénès
2020-02-25	Use implicit arguments in notations for eq.	Gaëtan Gilbert
2020-02-19	Only parsing in Reserved Notation: turning notice into a warning.	Hugo Herbelin
2020-02-19	Choosing a standard format for the "rew dependent" notation.	Hugo Herbelin
2020-02-18	Merge PR #11529: [build] Consolidate stdlib's .v files under a single directory.	Théo Zimmermann
2020-02-17	Merge PR #11350: stdlib List: add [remove'] and [count_occ'] that use [filter]	Hugo Herbelin
2020-02-13	[build] Consolidate stdlib's .v files under a single directory.	Emilio Jesus Gallego Arias
2020-02-08	Remove -compat 8.9.	Théo Zimmermann
2020-02-08	Merge PR #11240: Add rew dependent Notations	Hugo Herbelin
2020-02-06	replace RList by list R	Yves Bertot
2020-01-17	Fix issue #11396 : Rlist hides standard list constructors cons and nil	Michael Soegtrop
2020-01-14	Merge PR #11249: [stdlib] Additional statements in List.v	Hugo Herbelin
2020-01-08	Avoid hardcoded paths in extraction	Maxime Dénès
2020-01-06	stdlib List: add [remove'] and [count_occ']	Yishuai Li
2020-01-05	apply suggestions of @anton-trunov	Olivier Laurent
2020-01-05	clean some indentations	Olivier Laurent
2019-12-26	Add rew dependent Notations	Jason Gross
2019-12-24	Add statements with output in Type	Olivier Laurent
2019-12-23	Merge PR #10760: Make rapply handle all numbers of underscores	Pierre-Marie Pédrot
2019-12-17	[micromega] fix efficiency regression	Frédéric Besson
2019-12-14	Being explicit on existence of a remote link.	Hugo Herbelin
2019-12-06	Merge PR #11127: Added theorem Nat.bezout_comm.	Hugo Herbelin