coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	...	fkirchne	2010-05-28
*	Correction program_simplify. Devrait corriger certaines contribs.	aspiwack	2010-05-28
*	Generalized the formulation of classic_set in propositional contexts	herbelin	2010-05-28
*	Minor fix in doc chapter on inference rules (added a missing space).	herbelin	2010-05-28
*	Documentation of pretype_id (minor commit).	herbelin	2010-05-28
*	Fixing Derive Inversion for new proof engine	herbelin	2010-05-26
*	Added UIP_dec on suggestion of Eelis on #coq irc.	herbelin	2010-05-22
*	Extract Inductive is now possible toward non-inductive types (e.g. nat => int)	letouzey	2010-05-21
*	Added examples for checking that the guard condition excludes subterms	herbelin	2010-05-20
*	Fix bug 2307	pboutill	2010-05-20
*	fixed guard check with commutative cuts	barras	2010-05-20
*	Mrec was not substituted correctly	barras	2010-05-20
*	Ocamlbuild: various fix	letouzey	2010-05-19
*	Add (almost) compatibility with camlp4, without breaking support for camlp5	letouzey	2010-05-19
*	Nicer representation of tokens, more independant of camlp*	letouzey	2010-05-19
*	Remove refutpat.ml4, ideal.ml4 is again a normal .ml, let* coded in a naive way	letouzey	2010-05-19
*	static (and shared) camlp4use instead of per-file declaration	letouzey	2010-05-19
*	Discontinue support for ocaml 3.09.*	letouzey	2010-05-19
*	Remove compile-command pragmas for emacs	letouzey	2010-05-19
*	Some ocamldoc comments + Fixing name of .coqrc.version file in refman	pboutill	2010-05-18
*	Applicative commutative cuts in Fixpoint guard condition	pboutill	2010-05-18
*	Improved the efficiency of evars traverals thanks to a split of	herbelin	2010-05-13
*	Missing warning flush in a lexer message + update of CHANGES	herbelin	2010-05-12
*	Backporting r13007 (evar_merge wrong and costly) to V8.3 and added test.	herbelin	2010-05-10
*	Fix: Pfedit.get_current_goal_context when no goal is focused.	aspiwack	2010-05-10
*	Removed an evar_merge in clenv_fchain which not only is incorrect but	herbelin	2010-05-10
*	Removed $Id$ introduced inadvertently in r13005 (no more $Id$ since r12972)	herbelin	2010-05-09
*	Added a few informations about file lineages (for the most part in kernel)	herbelin	2010-05-09
*	Update of credits files	herbelin	2010-05-09
*	Fix bug #2315 : printing of defined evars in Coqide.	aspiwack	2010-05-07
*	Deux commentaires retirés de ocamldoc.	aspiwack	2010-05-07
*	better detection of nested recursion in Function	jforest	2010-05-07
*	Correction of a bug pointed by P. Casteran.	jforest	2010-05-07
*	Trying to find a problem pointed by P. Casteran	jforest	2010-05-07
*	term matching in ltac was not coherent with match goal in presence of wildcar...	jforest	2010-05-06
*	Correction in Function documentation	jforest	2010-05-06
*	Patch bug 2313.	soubiran	2010-05-05
*	Pfedit.resume_proof doesn't implicitly Pfedit.suspend_proof	pboutill	2010-05-05
*	- Fixing bug #2308 about Lemma ... with	vsiles	2010-05-04
*	Correction of bug 2290 (removing stupid message)	jforest	2010-05-04
*	Correction of bug 2290	jforest	2010-05-04
*	ocamldoc related fixes	pboutill	2010-05-03
*	Re-enable validation in "make check", run it in parallel with test-suite	glondu	2010-05-03
*	Fix discrimination of sorts which doesn't play well with cumulativity	msozeau	2010-05-02
*	Extraction: fix type_expunge_from_sign broken in last commit	letouzey	2010-05-01
*	Extraction: an experimental command to get rid of some cst/constructor arguments	letouzey	2010-04-30
*	Fail: a way to check that a command is refused without blocking a script	letouzey	2010-04-30
*	"make source-doc" builds documentation of mli in html and pdf at	pboutill	2010-04-29
*	After the approval of Bruno, here the patch for the checker.	soubiran	2010-04-29
*	Various minor improvements of comments in mli for ocamldoc	letouzey	2010-04-29