coq - The formal proof system

Age	Commit message (Expand)	Author
2013-07-06	Fixing a bug in the native compiler, introduced by r16363, leading to undefined	mdenes
2013-04-29	Merging Context and Sign.	ppedrot
2013-04-29	Splitting Term into five unrelated interfaces:	ppedrot
2013-03-25	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-13	Restrict (try...with...) to avoid catching critical exn (part 8)	letouzey
2013-03-12	invalid_arg instead of raise (Invalid_argement ...)	letouzey
2013-03-05	More monomorphization.	ppedrot
2013-02-26	kernel/declarations becomes a pure mli	letouzey
2013-02-26	Names: shortcuts for building {kn, constant, mind} with empty sections	letouzey
2013-02-18	use List.rev_map whenever possible	letouzey
2013-02-11	Fixing bug in native compiler with let patterns in fixpoint definitions.	mdenes
2013-01-28	Uniformization of the "anomaly" command.	ppedrot
2013-01-28	native_compute: Fixed dependencies compilation order.	mdenes
2013-01-22	New implementation of the conversion test, using normalization by evaluation to	mdenes