coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Rename rawterm.ml into glob_term.ml	glondu	2010-12-23
*	Change of nomenclature: rawconstr -> glob_constr	glondu	2010-12-23
*	Prepare change of nomenclature rawconstr -> glob_constr	glondu	2010-12-23
*	More precise documentation for instantiate	glondu	2010-12-23
*	Extraction: avoid type-unsafe optimisation of pattern-matchings (fix #2413)	letouzey	2010-12-21
*	Fixing bug #2454: inversion predicate strategy for inferring the type	herbelin	2010-12-19
*	Univ: try to avoid a few lookup in the universe graph	letouzey	2010-12-18
*	Univ.constraints made fully abstract instead of being a Set of abstract stuff	letouzey	2010-12-18
*	Revert last commit 13723 on Univ : minor gains and more complex code	letouzey	2010-12-18
*	Univ: an attempt to lazily compact chains of Equiv in a functionnal way	letouzey	2010-12-17
*	NPeano.modulo : another trick a la "minus" for having a decreasing arg	letouzey	2010-12-17
*	Cosmetic : let's take advantage of the n-ary exists notation	letouzey	2010-12-17
*	Nicer log2 function for nat (suggested by Hugo)	letouzey	2010-12-17
*	Univ: two improvements (speed + space)	letouzey	2010-12-16
*	Clenv.connect_clenv without its Evd.fold	letouzey	2010-12-15
*	Evar-related speed-up and clarifications in Class_tactics and Rewrite	letouzey	2010-12-15
*	Misc improvements about evar_map	letouzey	2010-12-15
*	Add improved indenters that rely on the current proof state to choose the ind...	gmelquio	2010-12-14
*	Add navigation items for quickly moving between word occurrences.	gmelquio	2010-12-14
*	Improved the search/replace dialog box:	gmelquio	2010-12-14
*	Fix mutex being released from a different thread than it is acquired from.	gmelquio	2010-12-14
*	Remove an unused function with a Evd.fold in subtac	letouzey	2010-12-13
*	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