coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Applied Cédric Auger's patch to fix use of "#&xxx;" in html printing	herbelin	2010-04-09
*	Commit 12906 continued (forgotten file).	herbelin	2010-04-07
*	Granting wish #2251 thanks to commit 12900 solved bug 1416.v (which	herbelin	2010-04-07
*	New model for user-driven translation of tokens in coqdoc	herbelin	2010-04-06
*	Improving compatibility between 8.2 and 8.3	herbelin	2010-04-05
*	Fix configure script: natdynlink works without a hack on 10.6.3.	msozeau	2010-04-05
*	Added a function in typing.ml to solve evars of a constr w/o going back down ...	herbelin	2010-04-05
*	Changement de ide/proofs.ml en ide/ideproofs.ml pour éviter un conflit	aspiwack	2010-04-05
*	Granting wish #2251 (forbidding rewriting a term reduced to an evar)	herbelin	2010-04-05
*	Tests for bug report #2244 (pattern-unification with abstraction over Meta's)	herbelin	2010-04-05
*	Partial fix to bug #2244 (ensure that pattern unification does not	herbelin	2010-04-05
*	Add documentation on the treatment of [if] and [let (x1, ... xn) := ..]	msozeau	2010-03-31
*	Small things about coqdoc + fixing lettuple.v test (part of bug #2289)	herbelin	2010-03-30
*	Removed hard-wiring of latin1 letters in coqdoc (see bug #2275)	herbelin	2010-03-30
*	Small improvements around coqdoc (including fix for bug #2288)	herbelin	2010-03-30
*	Fixed small bugs introduced in commit 12890 (bug #2286, that comes	herbelin	2010-03-30
*	Manual qualification of Mfourier.Proof in micromega to avoid ocamldep using i...	letouzey	2010-03-30
*	Improving error messages in the presence of utf-8 characters	herbelin	2010-03-30
*	Several bug-fixes and improvements of coqdoc	herbelin	2010-03-29
*	Extended on-the-fly eta-expansion in coercion mechanism to sort-polymorphic	herbelin	2010-03-28
*	Fixing bug #2254 (inappropriate names of Zlt_gt_succ and Zlt_succ_gt)	herbelin	2010-03-28
*	Fixing bug #2279 (printing nested let-in was in exponential time)	herbelin	2010-03-27
*	Applied greenrd's patch to fix bug 2255 (injection failed to	herbelin	2010-03-27
*	Fixed bug #2260 (check of resolution of all evars in the declaration	herbelin	2010-03-24
*	Updated CHANGES wrt 8.3	herbelin	2010-03-23
*	Added automatic expansion on the left of recursive notations	herbelin	2010-03-23
*	Changing types to reflect futur separation between toplevel and ide.	vgross	2010-03-23
*	infrastructure for safe marshal-based IPC	vgross	2010-03-23
*	Goal generation deported into ide/coq.ml, single function to obtain	vgross	2010-03-23
*	New functions for goals fetching.	vgross	2010-03-23
*	Fix bug in backtracking.	vgross	2010-03-23
*	debugging	vgross	2010-03-23
*	Removing unexpected printing of debug output (see bug report #2271).	herbelin	2010-03-19
*	Définition de GRAMMARCMA: parsing/grammar.cma n'était plus installé, ce qu...	notin	2010-03-19
*	kills a warning about vo in checker/safe_typing	letouzey	2010-03-18
*	Makefile.build: (slightly) more robust sed invocation for parsing camlp4deps/...	letouzey	2010-03-18
*	Myocamlbuild: slight simplification of code for .ml4	letouzey	2010-03-18
*	Oops, don't use zeta by default.	msozeau	2010-03-15
*	Stop dropping evar constraints when building a new goal evar defs.	msozeau	2010-03-15
*	Fix splitting evars tactics and stop dropping evar constraints when	msozeau	2010-03-15
*	fixed minor pbs with test cases	barras	2010-03-12
*	fixed confusion between number of cstr arguments and number of pattern variab...	barras	2010-03-12
*	introduced lazy computation of size info in the guard condition	barras	2010-03-11
*	Update manual on search commands	puech	2010-03-11
*	Minimal test suite for search commands	puech	2010-03-11
*	fix [Search] when the result has no hypothesis & constant comparison	puech	2010-03-11
*	No delta-reduction in libtypes anymore	puech	2010-03-11
*	Filter out "_subproof" objects from search results	puech	2010-03-11
*	NMake: remove useless tactics abstract_pair, nicer comments	letouzey	2010-03-10
*	NMake: Reorganization, interface for NMake_gen, explicit View, tactic destr_t...	letouzey	2010-03-10