coq - The formal proof system

Age	Commit message (Expand)	Author
2014-05-06	- Rename eq to equal in Univ, document new modules, set interfaces.	Matthieu Sozeau
2014-05-06	This commit adds full universe polymorphism and fast projections to Coq.	Matthieu Sozeau
2014-04-28	Adding a field ci_cstr_nargs to case_info and mind_consnrealargs to	Hugo Herbelin
2014-04-24	Adding a [fold_map] operation on constrs.	Pierre-Marie Pédrot
2014-03-05	Remove some dead-code (thanks to ocaml warnings)	Pierre Letouzey
2014-03-05	Remove many superfluous 'open' indicated by ocamlc -w +33	Pierre Letouzey
2014-03-03	Removing generic hashes in kernel.	Pierre-Marie Pédrot
2014-03-02	Fixing generic Hashtbl.hash in Constr.	Pierre-Marie Pédrot
2013-11-04	Using allocation-free version of Array higher-order function in critical	ppedrot
2013-10-27	More sharing in Constr.map_with_binders.	ppedrot
2013-10-24	Specializing hash functions for widely used types.	ppedrot
2013-10-22	Various optimizations in Constr, such as term sharing and allocation	ppedrot
2013-09-27	Removing a bunch of generic equalities.	ppedrot
2013-09-19	Get rid of the uses of deprecated OCaml elements (still remaining compatible ...	xclerc
2013-09-18	At least made the evar type opaque! There are still 5 remaining unsafe	ppedrot
2013-08-22	More complete hashcons : lists (dirpath), arrays (constr)	letouzey
2013-04-29	Splitting Term into five unrelated interfaces:	ppedrot