coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-07-18
\|\
\| *	Modules: fix bug #4294	Matthieu Sozeau	2015-07-16
\| *	Univs/Inductive: fix typechecking of cases	Matthieu Sozeau	2015-07-15
\| *	Unused variables reported by OCaml.	Hugo Herbelin	2015-07-10
\| *	Option -type-in-type: added support in checker and making it contaminating	Hugo Herbelin	2015-07-10
\| *	Native compiler: make non-fatal linking errors silent except in debug mode.	Maxime Dénès	2015-07-10
\| *	Native compiler: refactor code handling pre-computed values.	Maxime Dénès	2015-07-10
\| *	Kernel/Checker: Cleanup fixes of substitutions due to let-ins.	Matthieu Sozeau	2015-07-09
\| *	Kernel: primitive projections handling of let-ins	Matthieu Sozeau	2015-07-09
\| *	Improve semantics of -native-compiler flag.	Maxime Dénès	2015-07-09
\| *	Template polymorphism: A bug-fix for Bug #4258	mlasson	2015-07-09
\| *	Univs: bug fix.	Matthieu Sozeau	2015-07-07
* \|	Merge branch 'v8.5' into trunk	Maxime Dénès	2015-07-06
\|\\|
\| *	Fixing documentation (see Maxime's mail on coqdev, July 3).	Hugo Herbelin	2015-07-05
\| *	Fix handling of primitive projections in VM.	Maxime Dénès	2015-07-05
\| *	Fix convertibility of primitive projections for native_compute.	Maxime Dénès	2015-07-03
* \|	Merge branch 'v8.5' into trunk	Maxime Dénès	2015-07-02
\|\\|
\| *	More robust pattern matching on structured constants in VM.	Maxime Dénès	2015-07-02
\| *	Display functions for primitive projections.	Maxime Dénès	2015-07-02
\| *	Further simplification of the graph traversal in Univ.	Pierre-Marie Pédrot	2015-07-01
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-06-28
\|\\|
\| *	Share prop/set values in sorts.ml.	Matthieu Sozeau	2015-06-26
\| *	BUGFIX: Three fixes for the price of 1 in sorts.ml:	Matthieu Sozeau	2015-06-26
\| *	Less closures makes the GC happy.	Pierre-Marie Pédrot	2015-06-24
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-06-24
\|\\|
\| *	Less closures makes the GC happy.	Pierre-Marie Pédrot	2015-06-23
\| *	Add a Set Dump Bytecode command for debugging purposes.	Maxime Dénès	2015-06-23
* \|	Document the positivity checker.	Arnaud Spiwack	2015-06-23
* \|	Merge remote-tracking branch 'forge/v8.5'	Pierre Boutillier	2015-06-22
\|\\|
* \|	All invocations to ocaml compilers go through ocamlfind	Pierre Boutillier	2015-06-22
\| *	Native compiler: do not catch exceptions not related to dynlink.	Maxime Dénès	2015-06-15
\| *	Fix native compilation of primitive projections. Closes #4210.	Maxime Dénès	2015-06-08
\| *	Making Coq compile with ocp-memprof.	Pierre-Marie Pédrot	2015-06-01
\|/
*	Fix bug #4159	Matthieu Sozeau	2015-05-27
*	Fixing bug #4201: The native compiler is not race-free.	Pierre-Marie Pédrot	2015-05-17
*	Disable precompilation for native_compute by default.	Guillaume Melquiond	2015-05-14
*	Fix my previous commit on ~polyprop	Pierre Letouzey	2015-05-12
*	Extraction: fix the detection of the "polyprop" situation	Pierre Letouzey	2015-05-12
*	Fix some ill-typed debugging code in the VM.	Guillaume Melquiond	2015-04-27
*	Tactical `progress` compares term up to potentially equalisable universes.	Arnaud Spiwack	2015-04-22
*	Fixing bug #4190.	Pierre-Marie Pédrot	2015-04-16
*	fix code and bound for SWITCH instruction.	Benjamin Gregoire	2015-03-30
*	use a more compact representation of non-constant constructors	Benjamin Gregoire	2015-03-27
*	allows the vm to deal with inductive type with 8388607 constant constructors ...	Benjamin Gregoire	2015-03-26
*	Fix bug 4157,	Benjamin Gregoire	2015-03-26
*	Fix vm compiler to refuse to compile code making use of inductives with	Matthieu Sozeau	2015-03-25
*	More clever representation of substituted Cemitcode.	Pierre-Marie Pédrot	2015-03-25
*	Fully fixing bug #3491 (anomaly when building _rect scheme in the	Hugo Herbelin	2015-03-25
*	Fixing computation of non-recursively uniform arguments in the	Hugo Herbelin	2015-03-24
*	Fixing wrong rel_context in checking positivity condition.	Hugo Herbelin	2015-03-24