coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	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
*	Extraction: avoid internal eta-reduction (fix #2570)	letouzey	2011-12-08
*	Fixing grammar resetting bug in the presence of levels initially empty	herbelin	2011-12-07
*	Adapting test Existentials to new numbering strategy of evars (r14764).	herbelin	2011-12-07
*	Fixing a bug of commit r13310 (activating coercions only when module	herbelin	2011-12-07
*	Html page titles	pboutill	2011-12-07
*	Vectors use a bit more the pattern matching compiler	pboutill	2011-12-07
*	Typo	pboutill	2011-12-07
*	Fixed a synchronization bug between coqtop and the CoqIDE command pane.	ppedrot	2011-12-06
*	fix Makefile.common handling of -byte-only	gareuselesinge	2011-12-06
*	Documentation of Arguments + implicits	gareuselesinge	2011-12-06
*	Documentation for Arguments + notation scopes	gareuselesinge	2011-12-06
*	Documentation for Arguments + simpl	gareuselesinge	2011-12-06
*	Minor fixes to Arguments	gareuselesinge	2011-12-06
*	Backtrack on synchronizing universe counter with reset	herbelin	2011-12-06
*	Registering universe and meta/evar counters as summaries so as to	herbelin	2011-12-05