coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Applying Jean-Baptiste Rouquier's FAQ update proposed on coqdev about	herbelin	2011-09-24
*	Completing r14448 and thus continuing r14407 (using Cast to propagate	herbelin	2011-09-24
*	Fix commit 14489: missing Coq. in dirpath	letouzey	2011-09-23
*	auto with nocore : disable the use of the core database (wish #2188)	letouzey	2011-09-23
*	Program: add some check_required_library (fix #2592) + some dead code removal	letouzey	2011-09-23
*	Remove specific hash-consing of Term.types (was unused anyway)	letouzey	2011-09-22
*	Hash-consing: attempt to stop hash-consing separately constr in declare.ml	letouzey	2011-09-22
*	Remove duplicated version of check_required_library.	letouzey	2011-09-22
*	test-suite : an additional message displayed by Notation2.v	letouzey	2011-09-22
*	Fix test-suite for s/Defining '\1' as keyword/Identifier '\1' now a keyword/.	letouzey	2011-09-22
*	Fixing bug #2606 (bad coqdoc processing of coq escaped in comments).	herbelin	2011-09-22
*	Makefile.doc: typo, index_url.txt should be index_urls.txt	letouzey	2011-09-19
*	Fix test-suite/ide for repository compiled without -local (fix #2600)	letouzey	2011-09-19
*	avoid dependency nightmare by creating coqdep_{lexer,common}.mli	letouzey	2011-09-18
*	doc/refman/Extraction.tex: no need to actually build euclid.ml	letouzey	2011-09-17
*	Euclid: make the proof transparent (example of extraction in stdlib)	letouzey	2011-09-17
*	Various fixes in the Makefiles	letouzey	2011-09-17
*	Omega: for non-arithmetical goals, try proving False from context (wish #2236)	letouzey	2011-09-16
*	Omega aware of Z.pred (fix #1912)	letouzey	2011-09-15
*	Re-allowing assumptions during proofs seems safe now (fix #2411)	letouzey	2011-09-15
*	coqc: Recognize option -force-load-proofs.	letouzey	2011-09-15
*	Names.make_mbid and co : convert from/to identifier (avoid some String.copy)	letouzey	2011-09-15
*	Adds a new command Show Goal (e.g. Show Goal "42") printing a goal using the...	aspiwack	2011-09-12
*	correction du bug 2047	jforest	2011-09-09
*	More twicks on hash-consing	letouzey	2011-09-08
*	Fix the hconsing of universes	letouzey	2011-09-07
*	make world now builds fake_ide (to please coq-bench)	letouzey	2011-09-06
*	Improved ltac code for zify (fix #2575).	letouzey	2011-09-06
*	test-suite/ide: misc improvement	letouzey	2011-09-06
*	Avoid registering λ and Π as keywords just for some private Local Notation	letouzey	2011-09-06
*	ide/preferences.ml: apparently no `META in Gdk.Tags.modifier	letouzey	2011-09-06
*	Ocamlbuild : build of fake_ide	letouzey	2011-09-06
*	fake_ide: a short program to mimic an ide talking to coqtop -ideslave	letouzey	2011-09-05
*	Coqide: new backtracking code, based on the Backtrack command	letouzey	2011-09-05
*	Ide_intf: slight reorganisation of the IDE api	letouzey	2011-09-05
*	Lib: remove strange code about backtracking to the current state	letouzey	2011-09-05
*	Lib.node: merge OpenedModtype and OpenedModule, same for Closed...	letouzey	2011-09-05
*	Remove code concerning the obsolete Set/Unset Undo	letouzey	2011-09-05
*	Util.error now creates UserError(_,msg) instead of UserError(str,str)	letouzey	2011-09-05
*	Extraction Implicit: fix the numbering of constructor arguments	letouzey	2011-09-05
*	Having added a special Cast for remembering the use of conversion	herbelin	2011-09-04
*	Bug 3596: ocamlbuild: coq_makefile now requires Unix	pboutill	2011-09-03
*	Bug 2589: Documentation patch of Hendrik Tews	pboutill	2011-09-02
*	Coq_makefile: bugfix in install rule	pboutill	2011-09-02
*	Automatic search of project file	pboutill	2011-09-01
*	Coq_makefile : bug when a project file is not in the current directory.	pboutill	2011-09-01
*	safe_prerr_endline in Minilib	pboutill	2011-09-01
*	Add option -f to coqide	pboutill	2011-09-01
*	Add preferences to say how to deal with a project file.	pboutill	2011-09-01
*	same_file in Minilib	pboutill	2011-09-01