coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
...
* \|	CLEANUP: kernel/context.ml{,i}	Matej Kosik	2016-01-11
\|/
*	Fix some typos.	Guillaume Melquiond	2015-10-13
*	Fixing some English misspelling.	Hugo Herbelin	2015-07-29
*	Native compiler: refactor code handling pre-computed values.	Maxime Dénès	2015-07-10
*	Fix native compilation of primitive projections. Closes #4210.	Maxime Dénès	2015-06-08
*	Removing dead code.	Pierre-Marie Pédrot	2015-02-02
*	Make native compiler handle universe polymorphic definitions.	Maxime Dénès	2015-01-17
*	Correct restriction of vm_compute when handling universe polymorphic	Matthieu Sozeau	2015-01-15
*	Update headers.	Maxime Dénès	2015-01-12
*	Cleaner interfaces for linking locations of native compiler.	Maxime Dénès	2014-11-12
*	No hash consing across calls to the native compiler.	Maxime Dénès	2014-10-24
*	A patch for printing "match" when constructors are defined with let-in	Hugo Herbelin	2014-10-20
*	Add a boolean to indicate the unfolding state of a primitive projection,	Matthieu Sozeau	2014-09-27
*	This commit adds full universe polymorphism and fast projections to Coq.	Matthieu Sozeau	2014-05-06
*	Fixing ml-doc.	Pierre-Marie Pédrot	2014-05-01
*	Fix exponential behavior in native compiler with retroknowledge.	Maxime Dénès	2014-04-09
*	Optimizing Int31 support in native compiler, by not tagging	Maxime Dénès	2014-04-09
*	Machine arithmetic operations for native compiler.	Maxime Dénès	2014-04-09
*	Full support for int31 values in native compiler.	Maxime Dénès	2014-04-09
*	Partial support for open terms in int31.	Maxime Dénès	2014-04-09
*	Had to split Nativelambda in two files because of Retroknowledge	Maxime Dénès	2014-04-09
*	Int31 literals in native compiler.	Maxime Dénès	2014-04-09
*	Fixing generic hashes and replacing them with proper ones.	Pierre-Marie Pédrot	2014-03-03
*	Hunting pervasive equality in native compiler. It seems they were used for	Pierre-Marie Pédrot	2014-03-01
*	Lazyconstr -> Opaqueproof	Enrico Tassi	2014-02-26
*	Support for evars and metas in native compiler.	Maxime Dénès	2013-12-30
*	Got rid of unused lazy flag in the native compiler.	Maxime Dénès	2013-12-29
*	Removing native_name reference from constant_body.	Maxime Dénès	2013-12-28
*	More monomorphic List.mem + List.assoc + ...	letouzey	2013-10-24
*	Specializing hash functions for widely used types.	ppedrot	2013-10-24
*	Turn many List.assoc into List.assoc_f	letouzey	2013-10-24
*	Removing a bunch of generic equalities.	ppedrot	2013-09-27
*	Fixing a bug in the native compiler, introduced by r16363, leading to undefined	mdenes	2013-07-06
*	Merging Context and Sign.	ppedrot	2013-04-29
*	Splitting Term into five unrelated interfaces:	ppedrot	2013-04-29
*	Native compiler: hash-consing of generated code and values.	mdenes	2013-03-25
*	Native compiler: Inlined constants are now compiled, fixing a bug reported by	mdenes	2013-03-25
*	Restrict (try...with...) to avoid catching critical exn (part 8)	letouzey	2013-03-13
*	invalid_arg instead of raise (Invalid_argement ...)	letouzey	2013-03-12
*	More monomorphization.	ppedrot	2013-03-05
*	kernel/declarations becomes a pure mli	letouzey	2013-02-26
*	Names: shortcuts for building {kn, constant, mind} with empty sections	letouzey	2013-02-26
*	use List.rev_map whenever possible	letouzey	2013-02-18
*	Fixing bug in native compiler with let patterns in fixpoint definitions.	mdenes	2013-02-11
*	Uniformization of the "anomaly" command.	ppedrot	2013-01-28
*	native_compute: Fixed dependencies compilation order.	mdenes	2013-01-28
*	New implementation of the conversion test, using normalization by evaluation to	mdenes	2013-01-22