coq - The formal proof system

Age	Commit message (Expand)	Author
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
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	Add extraction for primitive floats	Erik Martin-Dorel
2019-11-01	docs: Add refman+stdlib documentation	Erik Martin-Dorel
2019-11-01	[ssr] Refactor/Extend of under to support more relations	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-21	Improvements of zify	Frédéric Besson
2019-10-07	Call to update-compat.py.	Pierre-Marie Pédrot
2019-09-25	Merge PR #10713: Define morphisms of real numbers and accelerate Cauchy reals	Hugo Herbelin
2019-09-16	Define morphisms of real numbers and accelerate Cauchy reals	Vincent Semeria
2019-09-16	Re-implementation of zify	Frédéric Besson
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-31	Merge PR #9811: [stdlib] Remove deprecated module Zlogarithm	Emilio Jesus Gallego Arias
2019-07-26	[stdlib] Remove deprecated module Zsqrt_compat	Vincent Laporte
2019-07-26	[stdlib] Remove deprecated module Zlogarithm	Vincent Laporte
2019-07-22	[Extraction] Add support for primitive integers	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-04-01	Several improvements and fixes of Lia	Frédéric Besson
2019-03-14	Add StrictProp.v with basic SProp related definitions	Gaëtan Gilbert