coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-09-06
\|\
\| *	print universes when dumping bytecode.	Gregory Malecha	2015-09-03
\| *	Implementing Herbelin's fix for the "NonPar" bug	mlasson	2015-09-03
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-08-05
\|\\|
\| *	Fixing pop_rel_context.	Hugo Herbelin	2015-08-02
\| *	Reverting 16 last commits, committed mistakenly using the wrong push command.	Hugo Herbelin	2015-08-02
\| *	Fixing pop_rel_context	Hugo Herbelin	2015-08-02
\| *	A patch renaming equal into eq in the module dealing with	Hugo Herbelin	2015-08-02
\| *	Adding eq/compare/hash for syntactic view at	Hugo Herbelin	2015-08-02
\| *	Followup of 9f81b58551.	Pierre-Marie Pédrot	2015-07-30
\| *	Fixing bug #4289 (hash-consing only user part of constant not	Hugo Herbelin	2015-07-30
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-07-29
\|\\|
\| *	Fixing some English misspelling.	Hugo Herbelin	2015-07-29
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-07-27
\|\\|
\| *	a small amount of documentation on the virtual machine.	Gregory Malecha	2015-07-23
\| *	Fix incomplete pattern-matching.	Matthieu Sozeau	2015-07-22
* \|	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