coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Extraction: attempt to provide nice extraction of chars and strings for Ocaml	letouzey	2010-06-04
*	Ascii: simplier ascii_of_pos, conversion from/to N, proofs about nat-->ascii-...	letouzey	2010-06-04
*	Extraction: finish ExtrOcamlNatInt, add similar translation nat==>big_int	letouzey	2010-06-04
*	doc Nstaz updated	pottier	2010-06-04
*	Backported r13068 to branch v8.3 (whd_betaiota on inferred return	herbelin	2010-06-04
*	A new command Compute foo, shortcut for Eval vm_compute in foo	letouzey	2010-06-04
*	Grobner.v removed	pottier	2010-06-04
*	"Improved" the form of the inferred type of "match" by	herbelin	2010-06-03
*	Added command "Locate Ltac qid".	herbelin	2010-06-03
*	Avoid computing tactic printing tree (std_ppcmds) when printing not needed in	herbelin	2010-06-03
*	plugins/xml: kill two warnings	letouzey	2010-06-03
*	Ocamlbuild: try to speed-up error detection in .ml, by byte-compiling first	letouzey	2010-06-03
*	Ide_blob: avoid direct use of Stdpp for compatibility with new camlp4	letouzey	2010-06-03
*	Misc fixes related to new nsatz (and ocamlbuild)	letouzey	2010-06-03
*	Add unix.cma on camlp4 command-line in coq_makefile (Closes: #2326)	glondu	2010-06-03
*	nsatz ajoute	pottier	2010-06-03
*	ajout oublie	pottier	2010-06-03
*	plugin groebner updated and renamed as nsatz; first version of the doc of nsa...	pottier	2010-06-03
*	Fix xml test in non-local mode	glondu	2010-06-02
*	Do not link system library into installed .cma	glondu	2010-06-02
*	Fix typos	glondu	2010-06-02
*	Fix test-suite cleaning	glondu	2010-06-02
*	Extraction: start of a support library	letouzey	2010-06-02
*	added -args option to coqide to pass options to coqtops	vgross	2010-06-01
*	Cleanup: remove code specific for ocaml 3.06	letouzey	2010-06-01
*	restore handling of lexer errors	letouzey	2010-06-01
*	CoqIDE goes multiprocess	vgross	2010-05-31
*	More indirection.	vgross	2010-05-31
*	Introducing strong typing for IDE - toplevel IPC	vgross	2010-05-31
*	deporting Coq specific code from ide to toplevel.	vgross	2010-05-31
*	Modifying startup sequence	vgross	2010-05-31
*	New pass on inductive schemes	herbelin	2010-05-29
*	Typo in comment of proof.ml	herbelin	2010-05-29
*	A little bit of cleanup, and some annotations.	fkirchne	2010-05-28
*	Account for Stephane Glondu's remarks.	fkirchne	2010-05-28
*	Modify the test for csdp and associated message.	fkirchne	2010-05-28
*	Use existing functions to reimplement search_exe.	fkirchne	2010-05-28
*	...	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