coq - The formal proof system

Age	Commit message (Expand)	Author
2010-05-22	Added UIP_dec on suggestion of Eelis on #coq irc.	herbelin
2010-05-21	Extract Inductive is now possible toward non-inductive types (e.g. nat => int)	letouzey
2010-05-20	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-19	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-18	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-13	Improved the efficiency of evars traverals thanks to a split of	herbelin
2010-05-12	Missing warning flush in a lexer message + update of CHANGES	herbelin
2010-05-10	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-09	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-07	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-06	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-05	Patch bug 2313.	soubiran
2010-05-05	Pfedit.resume_proof doesn't implicitly Pfedit.suspend_proof	pboutill
2010-05-04	- 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-03	ocamldoc related fixes	pboutill
2010-05-03	Re-enable validation in "make check", run it in parallel with test-suite	glondu
2010-05-02	Fix discrimination of sorts which doesn't play well with cumulativity	msozeau
2010-05-01	Extraction: fix type_expunge_from_sign broken in last commit	letouzey
2010-04-30	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-29	"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	fixed bug #2224 (Error message in positivity check fixed)	vsiles
2010-04-29	Two forgotten $Id$ in last commit	letouzey
2010-04-29	Remove the svn-specific $Id$ annotations	letouzey
2010-04-29	Removed obsolete v7->v8 translation code (function check_same_type is	herbelin
2010-04-29	Move from ocamlweb to ocamdoc to generate mli documentation	pboutill
2010-04-28	Dont recompute the contents of the proof window when entering the	vgross