coq - The formal proof system

Age	Commit message (Expand)	Author
2011-10-07	ocamlbuild: Fix ocamlbuild compilation for changes to configure from r14500.	glondu
2011-10-05	Fixing Implicit Tactic mode damaged by commit r14496 (see also bug #2612).	herbelin
2011-10-05	When a pattern match, don't use the first matching term but an	herbelin
2011-10-05	Removing vernacular code mistakenly committed.	herbelin
2011-10-05	Fixing critical inductive polymorphism bug found by Bruno.	herbelin
2011-10-05	Force dependency of Reference-Manual.pdf over Reference-Manual.dvi	herbelin
2011-10-05	Use an ad-hoc monomorphic list in RelationClasses to avoid some universe cons...	letouzey
2011-10-05	It happens that the type inference algorithm (pretyping) did not check	herbelin
2011-10-02	Hash-consing of constr could share more	letouzey
2011-10-01	Updating some links in the FAQ	herbelin
2011-10-01	Moving never-used comments from Zhints.v to dev/doc so as not to	herbelin
2011-10-01	Fixing critical part of bug #2504. Not all inductive types in Type are	herbelin
2011-09-27	In Coq_config: get rid of coqsrc and make coqlib optional	glondu
2011-09-26	Added support for referring to subterms of the goal by pattern.	herbelin
2011-09-26	Generalizing subst_term_occ so that it supports an arbitrary matching	herbelin
2011-09-26	Adding subst_term up to conv	herbelin
2011-09-26	Moving implicit tactic support from Tacinterp to Pfedit and final evar	herbelin
2011-09-25	Polishing commits r14492, r14448 and r14407 (tactics propagate	herbelin
2011-09-25	Not hard-wiring camlp5 path in target source-doc!	herbelin
2011-09-24	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-23	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-22	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-19	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-18	avoid dependency nightmare by creating coqdep_{lexer,common}.mli	letouzey
2011-09-17	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-16	Omega: for non-arithmetical goals, try proving False from context (wish #2236)	letouzey
2011-09-15	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-12	Adds a new command Show Goal (e.g. Show Goal "42") printing a goal using the...	aspiwack
2011-09-09	correction du bug 2047	jforest
2011-09-08	More twicks on hash-consing	letouzey
2011-09-07	Fix the hconsing of universes	letouzey
2011-09-06	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