coq - The formal proof system

Age	Commit message (Expand)	Author
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-19	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-18	Fixed some printing bugs.	herbelin
2010-04-17	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-16	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-14	Removing redundant internal variants of apply tactic and simplification of ML...	herbelin
2010-04-13	Remove only *.v.log files in clean of test-suite/Makefile	glondu
2010-04-11	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-10	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-09	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-07	Commit 12906 continued (forgotten file).	herbelin
2010-04-07	Granting wish #2251 thanks to commit 12900 solved bug 1416.v (which	herbelin
2010-04-06	New model for user-driven translation of tokens in coqdoc	herbelin
2010-04-05	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	Added a function in typing.ml to solve evars of a constr w/o going back down ...	herbelin
2010-04-05	Changement de ide/proofs.ml en ide/ideproofs.ml pour éviter un conflit	aspiwack
2010-04-05	Granting wish #2251 (forbidding rewriting a term reduced to an evar)	herbelin