coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Adding a new Control file centralizing the control options of Coq.	Pierre-Marie Pédrot	2014-06-07
*	Make kernel reduction code parametric over the handling of universes,	Matthieu Sozeau	2014-06-06
*	Dedicated map module for type universes. It uses hashmaps, which are	Pierre-Marie Pédrot	2014-06-05
*	Removing dead code from Univ.	Pierre-Marie Pédrot	2014-06-05
*	- Force every universe level to be >= Prop, so one cannot "go under" it anymore.	Matthieu Sozeau	2014-06-04
*	- Fix hashing of levels to get the "right" order in universe contexts etc...	Matthieu Sozeau	2014-06-04
*	Fixing incorrect printf format.	Pierre-Marie Pédrot	2014-06-02
*	- Fix for commit 15999903f875f4b5dbb3d5240d2ca39acc3cd777 which disallowed some	Matthieu Sozeau	2014-05-28
*	- Fix in kernel conversion not folding the universe constraints	Matthieu Sozeau	2014-05-26
*	Update infer_conv to record trivial Prop <= Type i constraints that are neede...	Matthieu Sozeau	2014-05-26
*	Fix native_compute for systems with a limited size for the command line.	Guillaume Melquiond	2014-05-22
*	Revert "Decent error message when a constant is not found"	Enrico Tassi	2014-05-16
*	Decent error message when a constant is not found	Enrico Tassi	2014-05-16
*	Another try at close_proof that should behave better w.r.t. exception handling.	Matthieu Sozeau	2014-05-16
*	Rewritten the sorting algorithm for universes with a better complexity.	Pierre-Marie Pédrot	2014-05-13
*	Using Maps to handle imports in Safe_typing. The order is irrelevant indeed,	Pierre-Marie Pédrot	2014-05-11
*	Reuse universe level substitutions for template polymorphism, fixing performance	Matthieu Sozeau	2014-05-09
*	Avoid allocations in type_of_inductive	Matthieu Sozeau	2014-05-08
*	Fast-path equality of sorts in compare_constr*	Matthieu Sozeau	2014-05-08
*	Add missing case for primitive projection in fold_map.	Matthieu Sozeau	2014-05-06
*	Fix extraction taking a type in the wrong environment.	Matthieu Sozeau	2014-05-06
*	Find a more efficient fix for dealing with template universes:	Matthieu Sozeau	2014-05-06
*	Add doc on the new API for universe polymorphism and primitive projections	Matthieu Sozeau	2014-05-06
*	- Fix eq_constr_universes restricted to Sorts.equal	Matthieu Sozeau	2014-05-06
*	- Fix bug preventing apply from unfolding Fixpoints.	Matthieu Sozeau	2014-05-06
*	Adapt universe polymorphic branch to new handling of futures for delayed proofs.	Matthieu Sozeau	2014-05-06
*	Adapt Y. Bertot's path on private inductives (now the keyword is "Private").	Yves Bertot	2014-05-06
*	- Fix handling of polymorphic inductive elimination schemes.	Matthieu Sozeau	2014-05-06
*	Cleanup in constr, correct classification of polymorphic defs.	Matthieu Sozeau	2014-05-06
*	- Fix index-list to show computational relations for rewriting files.	Matthieu Sozeau	2014-05-06
*	Various fixes of universe polymorphism and projections when they're set.	Matthieu Sozeau	2014-05-06
*	- Fix Check to use the constraints inferred during type inference.	Matthieu Sozeau	2014-05-06
*	Improve universe/level comparison using hashes.	Matthieu Sozeau	2014-05-06
*	In kernel/univ.ml, better allocation behavior, better eq_univs function	Matthieu Sozeau	2014-05-06
*	Compat with ocaml 3.12	Matthieu Sozeau	2014-05-06
*	- Fix comparison of universes.	Matthieu Sozeau	2014-05-06
*	Better hashconsing of levels and universes, working with modules.	Matthieu Sozeau	2014-05-06
*	Be defensive in univ/eq_instances, raise an anomaly on incompatible instances.	Matthieu Sozeau	2014-05-06
*	Reinstate hashconsing of instances, faster globally.	Matthieu Sozeau	2014-05-06
*	Restore reasonable performance by not allocating during universe checks,	Matthieu Sozeau	2014-05-06
*	- Rename eq to equal in Univ, document new modules, set interfaces.	Matthieu Sozeau	2014-05-06
*	Fix interface for template polymorphism, cleaning up code in all typing algor...	Matthieu Sozeau	2014-05-06
*	Properly reinstate old-style polymorphism in the kernel and pretyping/retyping.	Matthieu Sozeau	2014-05-06
*	Initial work on reintroducing old-style polymorphism for compatibility (the s...	Matthieu Sozeau	2014-05-06
*	Correct rebase on STM code. Thanks to E. Tassi for help on dealing with	Matthieu Sozeau	2014-05-06
*	Rework handling of universes on top of the STM, allowing for delayed	Matthieu Sozeau	2014-05-06
*	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
*	Native compiler: hide compiled files in a .coq-native subdirectory.	Maxime Dénès	2014-04-29
*	Adding a field ci_cstr_nargs to case_info and mind_consnrealargs to	Hugo Herbelin	2014-04-28