coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Ajout notation [ x ; ... ; y ] dans list_scope. Changement de la	herbelin	2008-04-29
*	Suppression de la partie ML de la contrib correctness. Les fichiers	herbelin	2008-04-29
*	Correction d'un bug dans coq_makefile: génération des règles implicites en...	notin	2008-04-29
*	Fix eauto still using delta when it shouldn't (should make CoRN compile	msozeau	2008-04-29
*	reparation bug de compil introduit au precedent commit	jforest	2008-04-28
*	menage dans funind + deplaceemnt de recdef dans funind	jforest	2008-04-28
*	Backtrack on using metas eagerly in auto, only done in "new auto" for	msozeau	2008-04-28
*	Suite commit 10861	herbelin	2008-04-28
*	Petites corrections vis à vis des commits 10860, 10859, 10850	herbelin	2008-04-28
*	Quelques bricoles autour de l'unification:	herbelin	2008-04-27
*	Correction du bug des types singletons pas sous-type de Set	herbelin	2008-04-27
*	Suite r10857	herbelin	2008-04-27
*	Report des quelques modifs faites avec Pierre Letouzey sur les	herbelin	2008-04-27
*	- Backtrack sur option with_types suite à confusion sur l'utilisation	herbelin	2008-04-27
*	- Fix bug in unification not taking into account the right meta	msozeau	2008-04-27
*	- Backtrack sur extension de syntaxe pour pose qui rentre en conflit avec	herbelin	2008-04-26
*	Debug implementation of failing tactics in Morphism to allow earlier	msozeau	2008-04-26
*	Modif un peu gadget (??): on peut écrire "set (f n:=t)" pour	herbelin	2008-04-26
*	Adaptation des fichiers de micromega suite aux changements dans	notin	2008-04-25
*	Ajout de "Theorem id1 : t1 ... with idn : tn" pour partager la preuve	herbelin	2008-04-25
*	correction bug 1839	soubiran	2008-04-25
*	- Fix bug in eterm which was not taking filtered contexts in evars into	msozeau	2008-04-25
*	Remplacement de l'appel à interp_constr pour globaliser une constante	herbelin	2008-04-24
*	Fix bug #1844, generalize implementation to handle and combination of	msozeau	2008-04-24
*	- Add pretty-printers for Idpred, Cpred and transparent_state, used for	msozeau	2008-04-24
*	Ajout propriété svn:keywords aux nouveaux fichiers du commit 10840	herbelin	2008-04-24
*	Prise en compte des coercions dans les clauses "with" même si le type	herbelin	2008-04-23
*	correction d'un bug sur la compostion des substitutions induites par les alia...	soubiran	2008-04-23
*	correction du bug sur Parameter Inline que j'ai reouvert hier par inadvertance	soubiran	2008-04-23
*	Added frozen state after each command.	courtieu	2008-04-23
*	Backtrack on change of flags for elim, otherwise rewrite goes under	msozeau	2008-04-23
*	Change default eauto depth to 100 in setoid_rewrite, bump necessary	msozeau	2008-04-23
*	Test que la bibliothèque ZArith est chargée lors d'un appel à simplify, er...	notin	2008-04-22
*	correction bug 1839	soubiran	2008-04-22
*	fixed universes bug related to module inclusion	barras	2008-04-22
*	test module include w.r.t. universe constraints	barras	2008-04-21
*	added the .vo checker (with independent Makefile)	barras	2008-04-21
*	- Correct unification for the rewrite variant of setoid_rewrite,	msozeau	2008-04-21
*	- Parameterize unification by two sets of transparent_state, one for open	msozeau	2008-04-21
*	Addded the "Dump Tree" command.	cek	2008-04-21
*	corection bug #1837	soubiran	2008-04-21
*	Correction bug 1838 + doc modules.	soubiran	2008-04-21
*	Work on the "occurrences" tactic argument. It is now possible to pass	msozeau	2008-04-20
*	Add the ability to give a transparent_state for conversion, to	msozeau	2008-04-20
*	Test pour compilation native camlp5	herbelin	2008-04-19
*	Pour engendrer version.tex, adoption de printf qui, au contraire de	herbelin	2008-04-18
*	Correction bug 1835 + correction bug occur-check résultant en un	herbelin	2008-04-18
*	pbm avec echo	filliatr	2008-04-18
*	Bug squashing day !	msozeau	2008-04-17
*	No compatibility notations for andb and co (this restore a correct Print output)	letouzey	2008-04-17