coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Merge PR #761: deprecate Pp.std_ppcmds type and promote Pp.t instead	Maxime Dénès	2017-07-31
\|\
* \	Merge PR #746: Timing on ci via coq_makefile for various projects	Maxime Dénès	2017-07-31
\|\ \
* \ \	Merge PR #923: [api] Fix base_include LTAC parts.	Maxime Dénès	2017-07-28
\|\ \ \
* \ \ \	Merge PR #889: Removing template polymorphism for definitions.	Maxime Dénès	2017-07-28
\|\ \ \ \
* \ \ \ \	Merge PR #888: Stronger kernel types	Maxime Dénès	2017-07-28
\|\ \ \ \ \
* \ \ \ \ \	Merge PR #823: Async off in Windows by default in CoqIDE	Maxime Dénès	2017-07-28
\|\ \ \ \ \ \
* \ \ \ \ \ \	Merge PR #782: Update API for fiat	Maxime Dénès	2017-07-28
\|\ \ \ \ \ \ \
* \ \ \ \ \ \ \	Merge PR #852: Makefile: fails if some .vo or .cm* file has no source	Maxime Dénès	2017-07-28
\|\ \ \ \ \ \ \ \
\| \| \| \| \| \| * \| \|	[api] Fix base_include LTAC parts.	Emilio Jesus Gallego Arias	2017-07-27
\| \| \| \| \| \| \| \| *	deprecate Pp.std_ppcmds type alias	Matej Košík	2017-07-27
\| \| \| \| \| \| * \| \|	Fix TypeclassDebug.out after conflicting PR merges	Matthieu Sozeau	2017-07-26
\| \|_\|_\|_\|_\|/ / / \|/\| \| \| \| \| \| \|
* \| \| \| \| \| \| \|	Merge PR #918: Extraction: do not mix Haskell types Any and () (fix bugs 4844...	Maxime Dénès	2017-07-26
\|\ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \	Merge PR #910: Add [opam update] and online repository to gitlab CI script.	Maxime Dénès	2017-07-26
\|\ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \	Merge PR #886: Fixing what was presumably a typo in the naming conventions file	Maxime Dénès	2017-07-26
\|\ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \	Merge PR #902: Only perform profile initialization and printing when the flag...	Maxime Dénès	2017-07-26
\|\ \ \ \ \ \ \ \ \ \ \
\| \| \| \| \| \| \| \| \| * \| \|	Removing template polymorphism for definitions.	Pierre-Marie Pédrot	2017-07-26
\| \| \| \| \| \| \| \| \|/ / /
* \| \| \| \| \| \| \| \| \| \|	Merge PR #894: Fixing a little location bug with recursive binders	Maxime Dénès	2017-07-26
\|\ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \	Merge PR #882: Adding a V8.7 compatibility version number.	Maxime Dénès	2017-07-26
\|\ \ \ \ \ \ \ \ \ \ \ \
\| \| \| \| \| \| \| \| \| \| * \| \|	Avoiding a variable shadowing in the kernel.	Pierre-Marie Pédrot	2017-07-26
\| \| \| \| \| \| \| \| \| \| * \| \|	Statically ensuring that inlined entries out of the kernel have no effects.	Pierre-Marie Pédrot	2017-07-26
\| \| \| \| \| \| \| \| \| \| * \| \|	Further simplication: do not recreate entries for side-effects.	Pierre-Marie Pédrot	2017-07-26
\| \| \| \| \| \| \| \| \| \| * \| \|	Remove a horrendous hack in Declare to retrieve exported side-effects.	Pierre-Marie Pédrot	2017-07-26
\| \| \| \| \| \| \| \| \| \| * \| \|	More precise type of entries capturing their lack of side-effects.	Pierre-Marie Pédrot	2017-07-26
\| \| \| \| \| \| \| \| \| \| * \| \|	Using a record type for Cooking.result.	Pierre-Marie Pédrot	2017-07-26
\| \| \| \| \| \| \| \| \| \| * \| \|	More precise type for universe entries.	Pierre-Marie Pédrot	2017-07-26
\| \| \| \| \| \| \| \| \| \| \| \|/ \| \| \| \| \| \| \| \| \| \| \|/\|
* \| \| \| \| \| \| \| \| \| \| \|	Merge PR #885: Removing a dummy parameter in some FMapPositive statements.	Maxime Dénès	2017-07-26
\|\ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \	Merge PR #868: Fix debug trace of typeclasses eauto.	Maxime Dénès	2017-07-26
\|\ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \	Merge PR #845: Add Z.mod_div lemma to standard library.	Maxime Dénès	2017-07-26
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \| \|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|/ / \|/\| \| \| \| \| \| \| \| \| \| \| \| \|
* \| \| \| \| \| \| \| \| \| \| \| \| \|	Merge PR #905: [api] Remove type equalities from API.	Maxime Dénès	2017-07-26
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \	Merge PR #857: Extraction: various fixes related with bug 4720	Maxime Dénès	2017-07-26
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \	Merge PR #859: Extraction TestCompile	Maxime Dénès	2017-07-26
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \	Merge PR #808: [api] Put some order in API.mli	Maxime Dénès	2017-07-26
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \	Merge PR #750: Remove deprecated options of ./configure in 8.8	Maxime Dénès	2017-07-26
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
\| \| \| \| \| * \| \| \| \| \| \| \| \| \| \| \| \| \|	make sure that API-leaks cannot be reintroduced by mistake	Matej Košík	2017-07-26
* \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Makefile.ide: restore a coqide-binaries rule (fix bug 5667)	Pierre Letouzey	2017-07-25
\| \| \| \| \| * \| \| \| \| \| \| \| \| \| \| \| \| \|	[api] Remove type equalities from API.	Emilio Jesus Gallego Arias	2017-07-25
\| \| \| \|_\|/ / / / / / / / / / / / / / \| \| \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \|
\| \| * \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	[api] Put modules in order in API.{mli,ml}	Emilio Jesus Gallego Arias	2017-07-25
\| \|/ / / / / / / / / / / / / / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| \| \| \| \| \| \| \| * \| \| \| \|	Extraction: do not mix Haskell types Any and () (revert 8e257d4, fix bugs 484...	Pierre Letouzey	2017-07-25
\| \|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|/ / / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| \| \| * \| \| \| \| \| \| \| \|	Adding a V8.7 compatibility version number.	Hugo Herbelin	2017-07-21
\| \|_\|_\|_\|_\|_\|/ / / / / / / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \|
* \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Merge PR #897: Fix test suite on windows (wrt fake_ide and coq-makefile)	Maxime Dénès	2017-07-21
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \
\| * \| \| \| \| \| \| \| \| \| \| \| \| \| \|	PMP sold us a Timeout on Windows with 1s resolution. Trying to improve it.	Maxime Dénès	2017-07-21
\| \| \| \| \| \| \| \| \| \| \| * \| \| \| \|	Add [opam update] and online repository to gitlab CI script.	Gaëtan Gilbert	2017-07-21
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| *	Alternate way of doing timing on ci	Jason Gross	2017-07-21
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| *	Separate make from python script for HoTT	Jason Gross	2017-07-21
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| *	Display timing data travis for various projects	Jason Gross	2017-07-21
\| \| \| \| \| \| \| \| \| \| \| \| \|_\|_\|/ \| \| \| \| \| \| \| \| \| \| \| \|/\| \| \|
\| * \| \| \| \| \| \| \| \| \| \| \| \| \|	Install time command under Cygwin (required for timing scripts).	Maxime Dénès	2017-07-21
\| \| \| \| * \| \| \| \| \| \| \| \| \| \|	Extraction: fix bugs 5177 and 5240 (and also indirectly bug 4720)	Pierre Letouzey	2017-07-20
\| \| \| \| \| \|_\|_\|_\|_\|_\|/ / / / \| \| \| \| \|/\| \| \| \| \| \| \| \| \|
* \| \| \| \| \| \| \| \| \| \| \| \| \|	Merge PR #892: Improve do_split option of typeclass resolution	Maxime Dénès	2017-07-20
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \| \|_\|_\|_\|/ / / / / / / / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \|
\| \| * \| \| \| \| \| \| \| \| \| \| \|	fake_ide: do as coqide to find out coqtop path	Enrico Tassi	2017-07-20
\| \| * \| \| \| \| \| \| \| \| \| \| \|	coq_makefile: use System.exists_dir for better portability	Enrico Tassi	2017-07-20