coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Move the call to the computation of bytecode inside Cemitcodes.	Pierre-Marie Pédrot	2018-02-14
*	Abstract further the type of VM bytecode compilation.	Pierre-Marie Pédrot	2018-02-14
*	[api] Deprecate all legacy uses of Names in core.	Emilio Jesus Gallego Arias	2017-11-06
*	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-10-29
\|\
\| *	Adds support for the virtual machine to perform reduction of universe polymor...	Gregory Malecha	2015-10-28
* \|	Exporting a purely functional interface to bytecode patching.	Pierre-Marie Pédrot	2015-10-16
\|/
*	Fixing some English misspelling.	Hugo Herbelin	2015-07-29
*	Correct restriction of vm_compute when handling universe polymorphic	Matthieu Sozeau	2015-01-15
*	fixed bug 2580. Quick fix: copy emitcodes before patching it	barras	2011-08-01
*	Remove the "Boxed" syntaxes and the const_entry_boxed field	letouzey	2011-01-28
*	Various minor improvements of comments in mli for ocamldoc	letouzey	2010-04-29
*	Move from ocamlweb to ocamdoc to generate mli documentation	pboutill	2010-04-29
*	Delete trailing whitespaces in all .{v,ml} files	glondu	2009-09-17
*	Names.substitution (and related functions) and Term.subst_mps moved to	sacerdot	2004-11-16
*	Changement dans les boxed values .	gregoire	2004-11-12
*	COMMITED BYTECODE COMPILER	barras	2004-10-20