coq - The formal proof system

Age	Commit message (Expand)	Author
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-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-07-06	Primitive persistent arrays	Maxime Dénès
2020-05-18	Update to 8.13.	Théo Zimmermann
2020-05-16	Prove that classical reals implement constructive reals. Also move sums, min ...	Vincent Semeria
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-04	add order properties about bool	Olivier Laurent
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-01	- Adjusted definitions and lemmas for asin and acos to what has been discussed	Michael Soegtrop
2020-03-27	Cleanup stdlib reals. Use implicit arguments for ConstructiveReals. Move Cons...	Vincent Semeria
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
2019-11-27	[release] Update files for 8.12 release per release process.	Emilio Jesus Gallego Arias
2019-11-11	Run update-compat script with --release option.	Théo Zimmermann
2019-11-01	Merge PR #10022: [ssr] Generalize tactics under and over to any (Reflexive) r...	Enrico Tassi
2019-11-01	docs: Add refman+stdlib documentation	Erik Martin-Dorel
2019-10-27	Merge PR #10827: Replace classical reals quotient axioms by functional extens...	Hugo Herbelin
2019-10-24	Replace classical reals quotient axioms by functional extensionality. Define ...	Vincent Semeria
2019-10-07	Call to update-compat.py.	Pierre-Marie Pédrot
2019-09-16	Define morphisms of real numbers and accelerate Cauchy reals	Vincent Semeria
2019-08-19	Split ConstructiveRealsLUB and improve comments	Vincent Semeria
2019-08-08	Add interface of constructive real numbers, with an opaque implementation by ...	Vincent Semeria
2019-08-08	[ssr] Refactor under's Setoid generalization to ease stdlib2 porting	Erik Martin-Dorel
2019-08-05	Merge PR #10445: Split constructive and classical axioms for real numbers	Vincent Laporte
2019-07-26	[stdlib] Remove deprecated module Zsqrt_compat	Vincent Laporte
2019-07-26	[stdlib] Remove deprecated module Zlogarithm	Vincent Laporte
2019-07-17	Rename ConstructiveRIneq and ConstructiveRcomplete	Vincent Semeria
2019-07-16	Define constructive real numbers as Cauchy sequences of rational numbers. Red...	Vincent Semeria
2019-04-02	Remove -compat 8.7	Jason Gross
2019-03-14	Add StrictProp.v with basic SProp related definitions	Gaëtan Gilbert
2019-02-04	Primitive integers	Maxime Dénès
2019-01-24	Update -compat to support -compat 8.10	Jason Gross
2018-11-28	Add `String Notation` vernacular like `Numeral Notation`	Jason Gross
2018-11-16	Merge PR #8888: Proof runcountable rebase	Hugo Herbelin