coq - The formal proof system

Age	Commit message (Expand)	Author
2009-03-28	Rewrite of Program Fixpoint to overcome the previous limitations:	msozeau
2009-03-27	Remove unused mli files	letouzey
2009-03-22	Backport from v8.2 branch of 11986 (interpretation of quantified	herbelin
2009-03-20	Many changes in the Makefile infrastructure + a beginning of ocamlbuild	letouzey
2009-03-20	Directory 'contrib' renamed into 'plugins', to end confusion with archive of ...	letouzey
2009-03-17	- configure: affiche si le natdynlink est positionne	barras
2009-03-16	Cleaning/improving the use of the "in" clause (e.g. "unfold foo in H at 4"	herbelin
2009-03-14	Better mechanism for loading initial plugins	letouzey
2009-03-09	Optionally list opaque constants in addition to axions/variables in	msozeau
2009-03-04	Timeout message was not always displayed	barras
2009-03-04	commande Timeout + compaction des traces de debug_tactic	barras
2009-03-04	Backtrack sur la mémoïsation de nf_evar.	aspiwack
2009-02-27	=?utf-8?q?Tentative=20d'optimisation=20(en=20temps)=20sur=20[nf=5Fevar]=20et=...	aspiwack
2009-02-19	On remplace evar_map par evar_defs (seul evar_defs est désormais exporté	aspiwack
2009-02-11	Fix de divers petits problèmes d'installation	notin
2009-02-11	Report des revisions #11826, #11828 et #11829 de v8.2 vers trunk	notin
2009-02-03	Allow to turn contrib/subtac into a (nat)dynlink'able plugin	letouzey
2009-01-26	Revert changes in pcoq functions to restore compatibility with contribs	puech
2009-01-23	Petit nettoyage faisant suite au commit #11847 .	aspiwack
2009-01-19	Les records déclarés avec Record ne peuvent plus être récursifs (le	aspiwack
2009-01-19	- Structuring Numbers and fixing Setoid in stdlib's doc.	herbelin
2009-01-18	Backporting from v8.2 to trunk:	herbelin
2009-01-18	Getting rid of the previous implementation of setoid_rewrite which was	msozeau
2009-01-18	Last changes in type class syntax:	msozeau
2009-01-17	DISCLAIMER	puech
2009-01-14	Fixing #1960 (xml bug with external on goal variable) and #1961	herbelin
2009-01-14	Fixing/improving management of uniform prefix Local and Global	herbelin
2009-01-13	- Standardized prefix use of "Local"/"Global" modifiers as decided in	herbelin
2009-01-11	- Deactivation of dynamic loading on Mac OS 10.5 (see bug #2024).	herbelin
2009-01-06	Conversion du fichier 'revision' en un fichier .ml + correction d'un bug dans...	notin
2009-01-05	Completed 11745 (move of jprover to user contribs) and cleaned 11743	herbelin
2009-01-04	Bug dans commit 11743	herbelin
2009-01-04	Fixed bugs #2001 (search_guard was overwriting the guard index given	herbelin
2009-01-02	Made the debugger work again:	herbelin
2008-12-31	Moved parts of Sign to Term. Unified some names (e.g. decomp_n_prod ->	herbelin
2008-12-29	- Added support for subterm matching in SearchAbout.	herbelin
2008-12-26	- Suppression date dans configure du trunk	herbelin
2008-12-24	- coq_makefile: target install now respects the original tree structure	herbelin
2008-12-19	Nettoyage des variables Coq et amélioration de coqmktop. Les	notin
2008-12-17	Sequel of 11697: repair coqtop.byte when contribs are statically linked (+min...	letouzey
2008-12-16	Take advantage of natdynlink when available: almost all contribs become loada...	letouzey
2008-12-14	Generalized binding syntax overhaul: only two new binders: `() and `{},	msozeau
2008-12-09	About "apply in":	herbelin
2008-12-04	Correct handling of defined methods (let-ins) in instance declarations.	msozeau
2008-11-28	Inductive parameters: nicer doc examples and error message	letouzey
2008-11-23	- Synchronized subst_object with load_object (load_and_subst_objects)	herbelin
2008-11-23	Minor improvement to commit 11619	herbelin
2008-11-23	Fixed bug #2006 (type constraint on Record was not taken into account) +	herbelin
2008-11-22	Fixed bug in VernacExtend printing + missing vernacular printing rules +	herbelin
2008-11-22	- Fixed minor bug #1994 in the tactic chapter of the manual [doc]	herbelin