coq - The formal proof system

Age	Commit message (Expand)	Author
2021-04-19	Merge PR #14108: [zify] bugfix	Vincent Laporte
2021-04-16	[zify] bugfix	Frederic Besson
2021-04-12	[zify] More aggressive application of saturation rules	BESSON Frederic
2021-04-12	Merge PR #14061: [zify] better error reporting	Vincent Laporte
2021-04-12	[zify] better error reporting	BESSON Frederic
2021-04-06	Standardizing spacing for {\| ... \|} in two files.	Hugo Herbelin
2021-04-06	Typo in a micromega comment.	Hugo Herbelin
2020-12-15	Modify micromega/ZMicromega.v to compile with -mangle-names	Jasper Hugunin
2020-12-15	Catch up to where I was last time.	Jasper Hugunin
2020-11-18	[micromega] Simplex uses alternatively Gomory cuts and case splits	BESSON Frederic
2020-11-18	[micromega] Optimised cnf in case an hypothesis is trivially False.	BESSON Frederic
2020-11-16	Explicitly annotate all hint declarations of the standard library.	Pierre-Marie Pédrot
2020-11-09	Merge PR #13173: Lint stdlib with -mangle-names #4	coqbot-app[bot]
2020-10-26	Merge PR #12768: Granting wish #12762: warning on duplicated catch-all patter...	coqbot-app[bot]
2020-10-20	[zify] Use flag for Z.to_euclidean_division_equations.	Frédéric Besson
2020-10-20	[zify] Add support for Int63.int	Frédéric Besson
2020-10-11	Modify micromega/ZifyInst.v to compile with -mangle-names	Jasper Hugunin
2020-10-11	Modify micromega/ZifyClasses.v to compile with -mangle-names	Jasper Hugunin
2020-10-11	Modify micromega/Ztac.v to compile with -mangle-names	Jasper Hugunin
2020-10-11	Modify micromega/ZCoeff.v to compile with -mangle-names	Jasper Hugunin
2020-10-11	Modify micromega/RingMicromega.v to compile with -mangle-names	Jasper Hugunin
2020-10-11	Modify micromega/Tauto.v to compile with -mangle-names	Jasper Hugunin
2020-10-11	Modify micromega/Refl.v to compile with -mangle-names	Jasper Hugunin
2020-10-11	Modify micromega/EnvRing.v to compile with -mangle-names	Jasper Hugunin
2020-10-11	Modify micromega/OrderedRing.v to compile with -mangle-names	Jasper Hugunin
2020-10-05	Adapting theories to unused pattern-matching variable warning.	Hugo Herbelin
2020-08-26	Modify lia to work with -mangle-names	Jasper Hugunin
2020-06-20	Add a pre-hook mechanism for the `zify` tactic	Kazuhiko Sakaguchi
2020-06-14	Update zify documentation	Frédéric Besson
2020-06-14	fix according to review by @pi8027	Frédéric Besson
2020-06-14	Update theories/micromega/ZifyBool.v	Frédéric Besson
2020-06-14	[micromega] native support for boolean operators	Frédéric Besson
2020-05-09	Merge PR #11990: [micromega] use Coqlib.lib_ref to get Coq constants.	Maxime Dénès
2020-04-30	[zify] add support for Nat.le, Nat.lt and Nat.eq	Frédéric Besson
2020-04-17	ZArith: move lia hints to a dedicated module	Vincent Laporte
2020-04-03	Avoiding using a fixed introduction name in Ltac code of stdlib.	Hugo Herbelin
2020-04-01	[micromega] use Coqlib.lib_ref to get Coq constants.	Frédéric Besson
2020-03-21	Add module ZifyPow to avoid compatibility issue with 8.11.	Théo Zimmermann
2020-03-18	Update headers in the whole code base.	Théo Zimmermann
2020-03-03	[zify] efficiency improvements	Frédéric Besson
2020-02-13	[build] Consolidate stdlib's .v files under a single directory.	Emilio Jesus Gallego Arias