coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
...
*	Goal: preventively replace an Evd.fold by an equivalent Evd.fold_undefined	letouzey	2010-12-13
*	Class_tactics: avoid an Evd.fold taking ages in contrib ProjectiveGeometry	letouzey	2010-12-13
*	Avoid silent loss of data when closing an unsaved buffer.	gmelquio	2010-12-13
*	Sorry for the mistake in r13702	pboutill	2010-12-12
*	Attempt to preserve casts during a refine, especially VMcast	letouzey	2010-12-10
*	First release of Vector library.	pboutill	2010-12-10
*	Don't interpret VMcast as an ordinary type cast in Definition a := t <: T.	herbelin	2010-12-09
*	In passing, very quick uniformization of coqdoc headers in a few files.	herbelin	2010-12-09
*	ZArith: for uniformity, Zdiv2 becomes Zquot2 while Zdiv2' becomes Zdiv2	letouzey	2010-12-09
*	Example of a simple ML tactic (Hello world).	fkirchne	2010-12-09
*	Fixed status of ÷ and × in coqdoc (they were seen as letter instead of symb...	herbelin	2010-12-06
*	Numbers and bitwise functions.	letouzey	2010-12-06
*	Use !Pp_control.std_ft for printing grammars	glondu	2010-12-06
*	Made new comm. model between coq and coqide support '-R foo ""'-style option.	herbelin	2010-12-04
*	Applied patch to FAQ proposed by Hendrik Tews (bug report #2446).	herbelin	2010-12-04
*	Fixing bug #2448 (wrongly-scoped alpha-renaming in notations).	herbelin	2010-12-04
*	Fixing coqdoc pretty-printing of a table in Mergesort. Incidentally,	herbelin	2010-12-04
*	Better fix to bug #2183 ("moduleid" internal name got exposed to users	herbelin	2010-12-04
*	Fixing several bugs with links to notation in coqdoc, including bug #2445:	herbelin	2010-12-04
*	Fixing bug using explictly declared implicit arguments in inductive arities.	herbelin	2010-12-03
*	Redirect stdout to stderr in -ideslave	glondu	2010-12-03
*	Remove dead code	glondu	2010-12-03
*	Fixing a bug introduced in r12304 (move of interpretation of	herbelin	2010-12-02
*	Document new tactics in CHANGES	glondu	2010-12-02
*	Documentation for tactic constr_eq	glondu	2010-12-02
*	Add tactic has_evar (#2433)	glondu	2010-12-02
*	Add tactic is_evar (Closes: #2433)	glondu	2010-12-02
*	* Kernel/Term:	regisgia	2010-12-01
*	* Kernel/Term	regisgia	2010-12-01
*	* Kernel/Term	regisgia	2010-12-01
*	Dp: minor fix suggested by Virgile Prevosto	letouzey	2010-11-25
*	CHANGES: mention some changes in trunk since the 8.3 fork	letouzey	2010-11-19
*	SearchAbout: who has never been annoyed by the [ ] syntax ?	letouzey	2010-11-19
*	CHANGES: small re-sync with the one of branch v8.3	letouzey	2010-11-19
*	adapt slighlty r13642 to support both camlp4 and camlp5-5 and camlp5-6	letouzey	2010-11-18
*	Some more revision of {P,N,Z}Arith + bitwise ops in Ndigits	letouzey	2010-11-18
*	Do not throw an error for anonymous generalized binders as they will be	msozeau	2010-11-18
*	NZSqrt: we define sqrt_up, a square root that rounds up instead of down as sqrt	letouzey	2010-11-18
*	NZLog: we define log2_up, a base-2 logarithm that rounds up instead of down a...	letouzey	2010-11-18
*	Support for camlp5 6.02.0 (Closes: #2432)	glondu	2010-11-16
*	Division: avoid imposing rem as an infix keyword in Z_scope and bigZ_scope.	letouzey	2010-11-16
*	Remove redundant clause (and fix compatibility issue)	glondu	2010-11-16
*	Use full path for unknown stuff in omega	glondu	2010-11-16
*	Minor fixes from Gregory Malecha. A typo fixed and a better (located)	msozeau	2010-11-15
*	Oups, fix last commit, a missing file in a vo.itarget	letouzey	2010-11-10
*	Integer division: quot and rem (trunc convention) in addition to div and mod	letouzey	2010-11-10
*	Refresh universes in params when generating schemes (Closes: #2429)	glondu	2010-11-08
*	Print universes in debugging printers	glondu	2010-11-08
*	Delayed the evar normalization in error messages to the last minute	herbelin	2010-11-07
*	Improved error messages in CoqIDE:	herbelin	2010-11-07