coq - The formal proof system

Age	Commit message (Expand)	Author
2009-03-18	fixed ring/field warning about hyp cleaning up	barras
2009-03-18	removed correctness dirs	barras
2009-03-18	coq_makefile: no ml dependency on coq sources	barras
2009-03-17	Uniformizing Tacticals, continued (allClauses -> allHypsAndConcl)	herbelin
2009-03-17	- gros commit sur ring et field: passage des arguments simplifie	barras
2009-03-17	Makefile:clean: rm *-mod.ml	barras
2009-03-17	- configure: affiche si le natdynlink est positionne	barras
2009-03-16	missing -c option of ocamlc in coq_makefile; coqdep_boot main loop was includ...	barras
2009-03-16	coqdep_boot: a specialized and dependency-free coqdep for killing one of the ...	letouzey
2009-03-16	Makefile: fix ignored errors, several attempts to clarify things	letouzey
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