coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Applying François Garillot's patch (#2261 in bug tracker) for extended	herbelin	2010-04-22
*	Ignore *.stamp files	herbelin	2010-04-22
*	Fixed bugs from commit 12954 on unification complexity	herbelin	2010-04-20
*	missing space in error message	vsiles	2010-04-20
*	Fixed bug #2999 (destruct was not refreshing universes of what it generalized *)	herbelin	2010-04-20
*	Propagated fix to bug 2127 (Hint Rewrite badly globalized in modules) to 8.2	herbelin	2010-04-20
*	Reduced the complexity of evar instantiations from O(n^3) to less than O(n^2).	herbelin	2010-04-19
*	In function "substitution_prefixed_by" the prefix test on module path	soubiran	2010-04-19
*	Fixed some printing bugs.	herbelin	2010-04-18
*	A pass on the CHANGES file + credits for 8.3 (completing commit 12906	herbelin	2010-04-17
*	Moved Case3.v from ideal features to success (it works since 8.2).	herbelin	2010-04-17
*	Solved a few problems of auto by bypassing the call to apply.	herbelin	2010-04-17
*	Use nice "unfold" instead of ugly "change" to display calls to unfold hints	herbelin	2010-04-17
*	cf. 12945	soubiran	2010-04-16
*	Extraction: cosmetics when using ocaml + Extract Inductive to symbols	letouzey	2010-04-16
*	Extraction: restore (temporarily?) a very limited form of linear letin reduction	letouzey	2010-04-16
*	Extraction: less eta in calls to global functions, better optimization phase	letouzey	2010-04-16
*	Names.mli: double declaration of mind_modpath	letouzey	2010-04-16
*	Extraction: improvement of optimizations (kill_dummy, optim_fix)	letouzey	2010-04-16
*	Util: remove list_split_at which is a clone of list_chop	letouzey	2010-04-16
*	Extraction: ad-hoc identifier type with annotations for reductions	letouzey	2010-04-16
*	Compare_dec : a few better proofs (and extracted terms), some more Defined	letouzey	2010-04-16
*	Extraction: less _ in Haskell (typically for False_rect), less toplevel eta-e...	letouzey	2010-04-16
*	Removing redundant internal variants of apply tactic and simplification of ML...	herbelin	2010-04-14
*	Remove only *.v.log files in clean of test-suite/Makefile	glondu	2010-04-13
*	Look for csdp in $PATH at runtime, remove -csdpdir configure option	glondu	2010-04-11
*	Remove unused functions run_sdpa	glondu	2010-04-11
*	Recovering 8.2 behavior of "simple (e)apply" (and hence of "(e)auto").	herbelin	2010-04-11
*	Run parallelized test-suite in "check" target of main Makefile	glondu	2010-04-10
*	Prettier test-suite/Makefile	glondu	2010-04-10
*	Optimized need for delimiters when disjoint scopes for strings and	herbelin	2010-04-10
*	Update .gitignore	glondu	2010-04-10
*	Use the Makefile in test-suite/check	glondu	2010-04-10
*	Makefile for the test-suite	glondu	2010-04-10
*	Fix typos in test-suite script	glondu	2010-04-10
*	Granting wish #2229 (InA_dec transparent) and Michael Day's coq-club	herbelin	2010-04-10
*	Test for bug #2231 (unexpected error when using let/if over an inductive	herbelin	2010-04-10
*	Partially fixed bug #2231 (an inductive parameter name was internally	herbelin	2010-04-10
*	Fixing various coqdep bugs (#2118, #2242, #2274)	herbelin	2010-04-10
*	Change definition of FSetList so that equality is Leibniz	glondu	2010-04-09
*	Add test-suite/lia.cache to .gitignore	glondu	2010-04-09
*	Fixing part 1 of bug #2242 (-I -as and -R -as were supported for	herbelin	2010-04-09
*	Granting wish #2249 (checking existing lemma name also when in a section).	herbelin	2010-04-09
*	Documenting the use of ##, %%, $$ in coqdoc.	herbelin	2010-04-09
*	Applied Cédric Auger's patch to fix use of "#&xxx;" in html printing	herbelin	2010-04-09
*	Commit 12906 continued (forgotten file).	herbelin	2010-04-07
*	Granting wish #2251 thanks to commit 12900 solved bug 1416.v (which	herbelin	2010-04-07
*	New model for user-driven translation of tokens in coqdoc	herbelin	2010-04-06
*	Improving compatibility between 8.2 and 8.3	herbelin	2010-04-05
*	Fix configure script: natdynlink works without a hack on 10.6.3.	msozeau	2010-04-05