coq - The formal proof system

Age	Commit message (Expand)	Author
2021-04-07	Merge PR #14008: [stdlib] [Arith] Cantor pairing	coqbot-app[bot]
2021-04-02	Remove the omega tactic and related options	Jim Fehrle
2021-04-02	add Cantor pairing to_nat and its inverse of_nat	Andrej Dudenhefner
2021-03-16	Adding a changelog and registering the new file in the documentation.	Pierre-Marie Pédrot
2021-03-06	Merge PR #13236: Add a type of format strings to Ltac2.	Michael Soegtrop
2021-03-03	[build] Split stdlib to it's own opam package.	Emilio Jesus Gallego Arias
2021-02-26	Signed primitive integers	Ana
2021-01-22	Add a type of format strings to Ltac2.	Pierre-Marie Pédrot
2020-12-02	Merge PR #13275: Put all Int63 primitives in a separate file	Vincent Laporte
2020-12-02	Put all Int63 primitives in a separate file	Pierre Roux
2020-11-23	Update compat infrastructure for 8.14	Enrico Tassi
2020-11-09	[compat] remove 8.10	Enrico Tassi
2020-11-05	[numeral notation] Specify R	Pierre Roux
2020-10-30	Renaming Numeral.v into Number.v	Pierre Roux
2020-10-20	[zify] Add support for Int63.int	Frédéric Besson
2020-07-06	Primitive persistent arrays	Maxime Dénès
2020-06-09	CReal: changed epsilon for modulus of convergence from 1/n to 2^z	Michael Soegtrop
2020-05-18	Update to 8.13.	Théo Zimmermann
2020-05-16	Merge PR #12288: Prove that classical reals implement constructive reals.	Michael Soegtrop
2020-05-16	Prove that classical reals implement constructive reals. Also move sums, min ...	Vincent Semeria
2020-05-15	Move SSR's Search to a new plugin and deprecate it.	Théo Zimmermann
2020-05-09	Hexadecimal: conversion to/from Coq strings	Pierre Roux
2020-05-09	Hexadecimal: proofs that conversions from/to nat,N,Z and Q are bijections	Pierre Roux
2020-05-09	[doc] Add hexadecimal numerals	Pierre Roux
2020-05-09	Decimal: specify numeral notation for Q	Pierre Roux
2020-05-07	Merge PR #12024: Fixes for LaTeX/html export of standard library in coqdoc	Théo Zimmermann
2020-05-04	add order properties about bool	Olivier Laurent
2020-04-24	Split off Nsatz tactic part into NsatzTactic	Jason Gross
2020-04-22	Merge PR #12031: [stdlib] A library on cyclic permutations: CPermutation	Hugo Herbelin
2020-04-21	Adding a Declare ML Module in empty file Ltac.v.	Hugo Herbelin
2020-04-19	A library on cyclic permutations: CPermutation	Olivier Laurent
2020-04-17	ZArith: move lia hints to a dedicated module	Vincent Laporte
2020-04-05	Adding package amssymb to support \lessgtr (apartness) in LaTeX output of coq...	Hugo Herbelin
2020-04-01	- Adjusted definitions and lemmas for asin and acos to what has been discussed	Michael Soegtrop
2020-03-30	Merge PR #11725: Cleanup stdlib reals.	Hugo Herbelin
2020-03-27	Cleanup stdlib reals. Use implicit arguments for ConstructiveReals. Move Cons...	Vincent Semeria
2020-03-27	Merge PR #11751: Fix #11749: don't warn for hidden files.	Maxime Dénès
2020-03-23	Merge PR #11442: Add module ZifyPow to avoid compatibility issue with 8.11.	Frédéric Besson
2020-03-21	Add module ZifyPow to avoid compatibility issue with 8.11.	Théo Zimmermann
2020-03-20	Build and install refman with Dune.	Théo Zimmermann
2020-03-04	Fix #11749: don't warn for hidden files.	Théo Zimmermann
2020-03-04	Add file to register names of reals library used by gappa	Michael Soegtrop
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-01-17	[doc] [dune] [ltac2] Build Ltac2 documentation [dune build system]	Emilio Jesus Gallego Arias
2020-01-08	Factorize ascii extraction in ExtrOcamlChar.v	Maxime Dénès
2020-01-08	Rename ExtrOcamlStringPlus into ExtrOcamlNativeString	Xavier Leroy
2020-01-08	Hide ExtrOcamlStringPlus.v like the other extraction files	Xavier Leroy
2019-12-17	[micromega] fix efficiency regression	Frédéric Besson
2019-11-27	[release] Update files for 8.12 release per release process.	Emilio Jesus Gallego Arias