coq - The formal proof system

Age	Commit message (Expand)	Author
2009-03-16	Makefile: minor improvements	letouzey
2009-03-16	Cleaning/improving the use of the "in" clause (e.g. "unfold foo in H at 4"	herbelin
2009-03-14	Cleaning/uniformizing the interface of tacticals.mli	herbelin
2009-03-14	Better mechanism for loading initial plugins	letouzey
2009-03-14	RefMan: a label defined twice	letouzey
2009-03-14	Makefile: ml dependencies of contribs are moved to .mllib files	letouzey
2009-03-14	Coqdep: better handling of Declare ML Module (via .mllib) + many cleanups	letouzey
2009-03-14	Coqdep: remove references to obsolete .zi and Require Implementation stuff	letouzey
2009-03-11	Cleanup: avoid the warning about Coq-tex not being a valid Ocaml module name	letouzey
2009-03-11	Cleanup: remove unused config/giveostype.ml	letouzey
2009-03-11	Cleanup: remove 3 unused files in ide/	letouzey
2009-03-11	Cleanup: remove old correctness files, unused for a long time	letouzey
2009-03-09	in natdynlink, lack of uniformity between general %.vo and Init/%.vo rules re...	barras
2009-03-09	Optionally list opaque constants in addition to axions/variables in	msozeau
2009-03-07	- per session coq command stack	vgross
2009-03-06	fixed groebner as a plugin + pattern matching Timeout	barras
2009-03-06	missing Require	barras
2009-03-06	oups (module Entiers remplace par Big_int)	barras
2009-03-05	ajout de la tactique groebner de Loic Pottier	barras
2009-03-04	illegal tactic application was having Ltac interpreter loop	barras
2009-03-04	doc et CHANGES pour la commande Timeout	barras
2009-03-04	removed unused state file	barras
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-03-04	Temporary hack to make coqide.byte work (backport r11948) (see #2062)	glondu
2009-03-04	fixes to typecheck with old lablgtk.	vgross
2009-03-03	Hack to fix compilation problems. will be removed on lablgtk upgrade.	vgross
2009-03-02	porting r11900 11905 and 11953 to trunk	barras
2009-03-02	Heavy modifications on the widget and edition tab creation mechanism.	vgross
2009-02-27	=?utf-8?q?Tentative=20d'optimisation=20(en=20temps)=20sur=20[nf=5Fevar]=20et=...	aspiwack
2009-02-27	extraction: update of README+CHANGES, rm of BUGS+TODO	letouzey
2009-02-27	Makefile: avoid building an empty contrib.cmxa	letouzey
2009-02-24	Amélioration de coq_makefile	notin
2009-02-23	Add support for dependent "destruct" over terms in dependent types.	herbelin
2009-02-20	CoqInterface.vo in CONTRIBVO (should fix a dependency issue)	letouzey
2009-02-20	On passe les last_mods (un des champs de Evd.evar_defs) de list	aspiwack
2009-02-20	On ne met plus rien dans les last_mods tant que conv_pbs est vide.	aspiwack
2009-02-20	coq-interface and coq-parser can be calls to coqtop with adequate code dynlink	letouzey
2009-02-19	On remplace evar_map par evar_defs (seul evar_defs est désormais exporté	aspiwack
2009-02-17	maj de la faq: correction de l'exemple field qui compilait plus en 8.2, corre...	jnarboux
2009-02-17	#rectypes was already automatically added when using 3.11	herbelin
2009-02-17	Made hack to have Drop and #use"include" working with ocaml 3.10 public	herbelin
2009-02-16	report de r11926: install de coqchk	barras
2009-02-16	Fix [apply_in] which short-circuited resolution of evars in a custom	msozeau
2009-02-13	Bug 2050, commit v8.2 11923-11924 ---> trunk	soubiran
2009-02-11	Backport of 11890 from branch v8.2 (compile tools with the best	herbelin
2009-02-11	Gestion des espaces dans les noms + guess_coqlib sous Windows	notin
2009-02-11	Nouvelle icône pour Coq	notin
2009-02-11	Fix d'un petit problème de chemin sous Windows	notin