coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
...
*	fixed bug #2224 (Error message in positivity check fixed)	vsiles	2010-04-29
*	Two forgotten $Id$ in last commit	letouzey	2010-04-29
*	Remove the svn-specific $Id$ annotations	letouzey	2010-04-29
*	Removed obsolete v7->v8 translation code (function check_same_type is	herbelin	2010-04-29
*	Move from ocamlweb to ocamdoc to generate mli documentation	pboutill	2010-04-29
*	Dont recompute the contents of the proof window when entering the	vgross	2010-04-28
*	Fix bug #2245, incorrect handling of Context in sections inside module	msozeau	2010-04-27
*	small detail about Scheme Equality	vsiles	2010-04-27
*	Added a new exception for already declared Schemes,	vsiles	2010-04-27
*	Misc small fixes : warning, dep cycles, ocamlbuild...	letouzey	2010-04-26
*	Disable ideal-features tests by default	glondu	2010-04-26
*	Here comes the commit, announced long ago, of the new tactic engine.	aspiwack	2010-04-22
*	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