coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
...
*	- Export de pattern_ident vers les ARGUMENT EXTEND and co.	herbelin	2008-10-19
*	Retour en arrière sur la mise en paramètre du premier argument de	herbelin	2008-10-19
*	Retour en arrière pour raison de compatibilité sur la suppression du nf_evar	herbelin	2008-10-19
*	Fixed bug #1966, wrong handling of evars.	msozeau	2008-10-18
*	Optimisation de clenv.ml pour que meta_instance ne soit pas appelé	herbelin	2008-10-18
*	Expérience de simplification de Ndigits compte tenu des tactiques existant	herbelin	2008-10-18
*	- Merge modifs coq_makefile.ml4 de la 8.1 vers le trunk (commit 11429)	herbelin	2008-10-18
*	Que Time n'empêche pas la colorisation des mots-clés.	herbelin	2008-10-18
*	Intégration et formattage du développement de Pierre Castéran sur les	herbelin	2008-10-18
*	Suppression de la dépendance de install-doc envers doc :	notin	2008-10-17
*	Extraction of Module with eq = ... : fix for bug #1853	letouzey	2008-10-16
*	Extraction of mutual types with alias: fix for bug #1965	letouzey	2008-10-16
*	Attempt to clarify Extract_env.extract_seb_spec	letouzey	2008-10-16
*	Report des commits 11417 et 11437 de la v8.2	soubiran	2008-10-15
*	report de la révision r11451 (nouveau style html pour le manuel de référence)	notin	2008-10-14
*	Dumpglob.dump_modref : fix an assert failure	letouzey	2008-10-14
*	test-suite: more utf8 tests, a test of ! ? and so on in rewrites	letouzey	2008-10-14
*	ugly comment erroneously left in the minus definition	letouzey	2008-10-14
*	Backporting 11445 from 8.2 to trunk (negative conditions in	herbelin	2008-10-11
*	* Fixed constr_cmp again to handle universes subtyping correctly	puech	2008-10-09
*	Fix bug #1959 (remember: never use a partial functions mindlessly).	msozeau	2008-10-08
*	Améliorations de l'affichage des coercions suggérées par Georges :	herbelin	2008-10-08
*	fixing r11433 again:	barras	2008-10-07
*	fixed pb with r11433	barras	2008-10-07
*	bug #1951: polymorphic indtypes: universe subst was not performed in the type...	barras	2008-10-06
*	## Lines starting with '## ' will be removed from the log message.	msozeau	2008-10-06
*	(Try to) use the conversion oracle also in w_unify to choose which constant to	msozeau	2008-10-03
*	Minor fixes related to coqdoc and --interpolate and the dependent	msozeau	2008-10-03
*	Fixing constr_cmp, propagating subtyping only right of a product	puech	2008-10-02
*	Correcting a delta normalization bug in VM (checked by benjamin)	jforest	2008-09-30
*	Forgot one file.	msozeau	2008-09-25
*	Improvements in coqdoc:	msozeau	2008-09-25
*	Various little improvements:	msozeau	2008-09-25
*	Partial fix for bug #1948: recompute order of dependencies between	msozeau	2008-09-25
*	Report change of the implicit argument status of the carrier type in the	msozeau	2008-09-16
*	Report improvements in Equations to the dependent elimination tactic:	msozeau	2008-09-15
*	Fix bug #1943 and restrict the inference optimisation of Program to	msozeau	2008-09-15
*	Add types introduced by subtac in *.glob files	glondu	2008-09-15
*	Update stdlib html template	glondu	2008-09-15
*	A pass on documentation:	msozeau	2008-09-14
*	Add user syntax for creating hint databases [Create HintDb foo	msozeau	2008-09-14
*	Use manual implicts in Classes and rationalize class parameter names.	msozeau	2008-09-14
*	In manual implicit arguments mode, do not enrich implicits	msozeau	2008-09-14
*	Fix bug #1931 by searching for a sort after doing beta,iota,delta-	msozeau	2008-09-14
*	Fix bug #1936: uncaught exception due to undefinable exceptions.	msozeau	2008-09-14
*	Fix bug #1939: defined evars were not substituted in some typeclasses	msozeau	2008-09-14
*	Fix bug #1940: uncaught exception when searching for a type class.	msozeau	2008-09-14
*	Finish debugging the unification machinery in [Equations]. Do the _comp	msozeau	2008-09-13
*	Remove redefinition of id in Program.Basics, just add maximal implicits.	msozeau	2008-09-13
*	Fix a bug, in fold_constr_with_binders, the types of fixpoints were	msozeau	2008-09-13