coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Directory 'contrib' renamed into 'plugins', to end confusion with archive of ...	letouzey	2009-03-20
*	coq_makefile: -c and -shared conflict; tacinterp: delay evaluation of tactic ...	barras	2009-03-19
*	renamed %-mod.ml into %_mod.ml to avoid ocaml warning	barras	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-18
*	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-17
*	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-16
*	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-14
*	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-11
*	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-09
*	- per session coq command stack	vgross	2009-03-07
*	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-06
*	ajout de la tactique groebner de Loic Pottier	barras	2009-03-05
*	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-04
*	Hack to fix compilation problems. will be removed on lablgtk upgrade.	vgross	2009-03-03
*	porting r11900 11905 and 11953 to trunk	barras	2009-03-02
*	Heavy modifications on the widget and edition tab creation mechanism.	vgross	2009-03-02
*	=?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-27
*	Amélioration de coq_makefile	notin	2009-02-24
*	Add support for dependent "destruct" over terms in dependent types.	herbelin	2009-02-23
*	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