coq - The formal proof system

Age	Commit message (Expand)	Author
2011-04-01	CHANGES: a word about recent changes in coqide, about Ctrl-C in vm	letouzey
2011-04-01	Checks for signals in VM, allowing it to be interrupted by Ctrl-C (experimental)	letouzey
2011-03-11	Tentative to make unification check types at every instanciation of an	msozeau
2011-03-08	adding eta in the vm	bgregoir
2011-03-05	Moving printing of module typing errors upwards to himsg.ml so as to	herbelin
2011-03-05	Starting being more explicit on the reasons why module subtyping fails.	herbelin
2011-03-05	Fixed a "feature" about subtyping records: one was expected not only	herbelin
2011-02-24	Mod_subst: improving sharing of subst_mps	letouzey
2011-02-23	Some more simplification in Mod_subst	letouzey
2011-02-17	- Use transparency information all the way through unification and	msozeau
2011-02-11	Mod_typing: some refactoring (common parts about MSEapply and co)	letouzey
2011-02-11	Safe_typing: some refactoring (avoiding copy-paste of record definitions)	letouzey
2011-02-11	Mod_subt: some more refactoring, substitution is also separated in two tables	letouzey
2011-02-11	Mod_subst: split delta_resolver in two tables (mp / kn)	letouzey
2011-02-11	compatibility <3.12 (Map.exists Map.singleton)	pboutill
2011-01-31	A fine-grain control of inlining at functor application via priority levels	letouzey
2011-01-28	Remove the "Boxed" syntaxes and the const_entry_boxed field	letouzey
2011-01-27	Make simpl use the proper constant when folding (mutual) fixpoints	letouzey
2011-01-25	Rewrite sort_universes to minimize the number of universes	glondu
2011-01-11	In univ.ml, put universe_level primitives in its their own sub-module	glondu
2011-01-11	Add "Print Sorted Universes"	glondu
2011-01-11	More coherent comment ordering	glondu
2010-12-19	Fixing bug #2454: inversion predicate strategy for inferring the type	herbelin
2010-12-18	Univ: try to avoid a few lookup in the universe graph	letouzey
2010-12-18	Univ.constraints made fully abstract instead of being a Set of abstract stuff	letouzey
2010-12-18	Revert last commit 13723 on Univ : minor gains and more complex code	letouzey
2010-12-17	Univ: an attempt to lazily compact chains of Equiv in a functionnal way	letouzey
2010-12-16	Univ: two improvements (speed + space)	letouzey
2010-12-01	* Kernel/Term:	regisgia
2010-12-01	* Kernel/Term	regisgia
2010-12-01	* Kernel/Term	regisgia
2010-11-15	Minor fixes from Gregory Malecha. A typo fixed and a better (located)	msozeau
2010-11-03	Correction bug 2427	soubiran
2010-11-03	Remove suspiciously named "implicit" stuff from Term	glondu
2010-11-03	In Univ, unify order_request and constraint_type	glondu
2010-11-02	More generic Univ.dump_universes	glondu
2010-10-05	Reintroduce kind_of_type (used by Presburger contrib)	glondu
2010-10-04	Forgotten lifts in eta-expansion	glondu
2010-10-03	Fixing printing of module_path names (was using a debugging	herbelin
2010-09-28	Remove kind_of_type, kind_of_term2 (dead code)	glondu
2010-09-24	Partial review of removed dead code (r13460)	herbelin
2010-09-24	Some dead code removal, thanks to Oug analyzer	letouzey
2010-09-23	Fix inconsistency in Prop/Set conversion check	glondu
2010-09-20	Added eta-expansion in kernel, type inference and tactic unification,	herbelin
2010-09-15	Sharing is not anymore broken by traverse_module.	soubiran
2010-09-15	Fix likely semantic typos	glondu
2010-08-27	* kernel/Safe_typing.LightenLibrary:	regisgia
2010-08-27	* (checker\|kernel)/Safe_typing:	regisgia
2010-08-27	* (checker\|kernel)/Safe_typing:	regisgia
2010-08-27	* checker/SafeTyping kernel/SafeTyping:	regisgia