coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Revert "Add [Polymorphic] flag for defs"	msozeau	2011-04-13
*	- Remove create_evar_defs	msozeau	2011-04-13
*	Fix merge.	msozeau	2011-04-13
*	- Do not make constants with an assigned type polymorphic (wrong unfoldings).	msozeau	2011-04-13
*	Add [Polymorphic] flag for defs	msozeau	2011-04-13
*	Subtyping: align coqtop behavior concerning opaque csts on coqchk's one	letouzey	2011-04-12
*	Replaced printing number of ill-typed branch by printing name of constructor	herbelin	2011-04-08
*	A few extra combinators about rel_declaration/named_declaration + a bit of doc	herbelin	2011-04-06
*	Lazy loading of opaque proofs: fast as -dont-load-proofs without its drawbacks	letouzey	2011-04-03
*	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-04-01
*	Tentative to make unification check types at every instanciation of an	msozeau	2011-03-11
*	adding eta in the vm	bgregoir	2011-03-08
*	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-03-05
*	Mod_subst: improving sharing of subst_mps	letouzey	2011-02-24
*	Some more simplification in Mod_subst	letouzey	2011-02-23
*	- Use transparency information all the way through unification and	msozeau	2011-02-17
*	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-02-11
*	A fine-grain control of inlining at functor application via priority levels	letouzey	2011-01-31
*	Remove the "Boxed" syntaxes and the const_entry_boxed field	letouzey	2011-01-28
*	Make simpl use the proper constant when folding (mutual) fixpoints	letouzey	2011-01-27
*	Rewrite sort_universes to minimize the number of universes	glondu	2011-01-25
*	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	2011-01-11
*	Fixing bug #2454: inversion predicate strategy for inferring the type	herbelin	2010-12-19
*	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-18
*	Univ: an attempt to lazily compact chains of Equiv in a functionnal way	letouzey	2010-12-17
*	Univ: two improvements (speed + space)	letouzey	2010-12-16
*	* Kernel/Term:	regisgia	2010-12-01
*	* Kernel/Term	regisgia	2010-12-01
*	* Kernel/Term	regisgia	2010-12-01
*	Minor fixes from Gregory Malecha. A typo fixed and a better (located)	msozeau	2010-11-15
*	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-03
*	More generic Univ.dump_universes	glondu	2010-11-02
*	Reintroduce kind_of_type (used by Presburger contrib)	glondu	2010-10-05
*	Forgotten lifts in eta-expansion	glondu	2010-10-04
*	Fixing printing of module_path names (was using a debugging	herbelin	2010-10-03
*	Remove kind_of_type, kind_of_term2 (dead code)	glondu	2010-09-28
*	Partial review of removed dead code (r13460)	herbelin	2010-09-24