coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
...
*	Version number, copyright, credits: missing updates.	herbelin	2011-12-25
*	Credits for 8.4: More exhaustive list of external contributors.	herbelin	2011-12-23
*	myocamlbuild: -DWIN32 instead of -DWin32	letouzey	2011-12-23
*	Configure: the backslashes in win32 paths should be escaped	letouzey	2011-12-23
*	Credits for 8.4 + resetting COMPATIBILITY file.	herbelin	2011-12-22
*	sequel of previous commit	letouzey	2011-12-21
*	Isolate a few types of Goptions in a pure .mli, solving a dep issue with ocam...	letouzey	2011-12-21
*	Pure interfaces shouldn't be mentionned in .mllib	letouzey	2011-12-21
*	adapt myocamlbuild after changes in coqdep_boot (.beautify)	letouzey	2011-12-21
*	Cleaning CHANGES file.	herbelin	2011-12-21
*	Notifying removal of accidental unfolding of recursive calls of	herbelin	2011-12-19
*	Arguments: check rename even if no implicit is specified	gareuselesinge	2011-12-19
*	test suite update after r14808	pboutill	2011-12-19
*	Bug 2377 part 2: old revision file is erased by install	pboutill	2011-12-19
*	Fixed some printing details for dependent evars in emacs mode. Patch	courtieu	2011-12-19
*	Granted legitimate wish #2607 (not exposing crude fixpoint body of	herbelin	2011-12-18
*	CoqIde files position is freedesktop compliant.	pboutill	2011-12-18
*	./configure & freedesktop	pboutill	2011-12-18
*	Fixing bug #2634 (unscoped notations were disturbing the	herbelin	2011-12-18
*	Applied patches proposed suggested by Hendrik Tews to fix existential	courtieu	2011-12-18
*	Continuing 14812 and 14813 (use type information to reduce the	herbelin	2011-12-18
*	Fixed a Not_found bug when declaring in a section some implicit	herbelin	2011-12-18
*	Removing PrintConstr debugging entry in g_proof.ml4 which was not	herbelin	2011-12-18
*	Suspending declaration of undefined debug printers.	herbelin	2011-12-18
*	Added a flag to control the use of typing when instantiating applied	herbelin	2011-12-17
*	Added ability to take the type of applied metas into account when	herbelin	2011-12-17
*	Reorganizing Unification.unify_0 so as to more easily share code	herbelin	2011-12-17
*	Command Arguments: standardizing format of error messages and American spelling.	herbelin	2011-12-17
*	Coq_makefile: "beautify" target	pboutill	2011-12-17
*	Coqdep adds %.v.beautified on the left of the ':' when it generates %.v depen...	pboutill	2011-12-17
*	Coq_makefile: "validate" target calls the checker over all vo.	pboutill	2011-12-17
*	Coq_makefile: section refactoring and no variables for OCaml if no ml* files ...	pboutill	2011-12-17
*	Coq_makefile: if no -install is provided, install location is set by a Makefi...	pboutill	2011-12-17
*	Deactivated automatic inference of _case schemes, as it was in 8.3	herbelin	2011-12-17
*	A pass on warning printings. Made systematic the use of msg_warning so	herbelin	2011-12-17
*	Bypassing the use of (currently unimplemented) "Show Script" in tests	herbelin	2011-12-17
*	Improving pretty-printing of Ltac functions.	herbelin	2011-12-17
*	Fixing format of complexity bug Notations.v.	herbelin	2011-12-17
*	Fixing previous commit which was bugging on tactics preceded by goal number (...	courtieu	2011-12-16
*	Coqide: adapt some comments now that bullets are terminators like { }	letouzey	2011-12-16
*	Introducing a notion of evar candidates to be used when an evar is	herbelin	2011-12-16
*	Fixing amazing loop when using eta-expansion in pattern-matching for	herbelin	2011-12-16
*	Adapting coqide to my last commit:	courtieu	2011-12-16
*	Moving bullets (-, +, *) into stand-alone commands instead of being	courtieu	2011-12-16
*	Cleaned up a bit goal handling in Coqtop interface. Now we have two queries :...	ppedrot	2011-12-15
*	Some extra universe refreshing seems needed in abstract_generalize	herbelin	2011-12-14
*	CHANGES: some more updates	letouzey	2011-12-12
*	Proof using ...	gareuselesinge	2011-12-12
*	Extraction: only do the test on generalizable lets for ocaml	letouzey	2011-12-10
*	Makefile: force the installation of all .cmi (and remove some obsolete .mli)	letouzey	2011-12-08