coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
...
*	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