coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Stop using a coqdocdoc env which prevents use of environments inside	msozeau	2008-10-26
*	- MAJ svn:ignore pour bin/coq-parser (anciennement bin/parser)	herbelin	2008-10-26
*	Backtrack sur commit 11467 (tentative d'optimisation meta_instance qui	herbelin	2008-10-26
*	More debugging of handling of open constrs with typeclasses:	msozeau	2008-10-25
*	Fix for bug #1981, correct the mismatch between the meta types used in	msozeau	2008-10-25
*	Raise informative errors instead of Failures or anomalies in case a meta	msozeau	2008-10-24
*	Fix doc of apply in (see coq-club message 26 September 2008)	herbelin	2008-10-24
*	Forgot one file which had other local modifications...	msozeau	2008-10-23
*	Fix bug #1977 by allowing the [apply] variants to take an [open_constr]	msozeau	2008-10-23
*	Open notation for declaring record instances.	msozeau	2008-10-23
*	Generalized implementation of generalization.	msozeau	2008-10-23
*	Fix bugs #1975 and #1976.	msozeau	2008-10-22
*	Fix for bug #1973 provided by Brian Campbell.	msozeau	2008-10-22
*	Various coqdoc improvements:	msozeau	2008-10-22
*	A much better implementation of implicit generalization:	msozeau	2008-10-22
*	Affichage des notations récursives:	herbelin	2008-10-22
*	More OCaml-3.11-friendly configure script	glondu	2008-10-21
*	warning message when a qualid to extract can be both a module or a cst	letouzey	2008-10-21
*	duplicated open of Ppconstr	letouzey	2008-10-21
*	Correction bug #1969.	soubiran	2008-10-21
*	Renommage "Global Instance" en "Instance Global" pour uniformisation	herbelin	2008-10-20
*	Zdiv: eqm (equality modulo some N) can now be declared as Parametric Relation	letouzey	2008-10-20
*	Syntaxe de COQBIN	notin	2008-10-20
*	Suite 11472 et 11473	herbelin	2008-10-19
*	Suite 11472	herbelin	2008-10-19
*	- 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