coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Apply vmconv if there are no _undefined_ evars around.	msozeau	2008-11-08
*	Slight change of the semantics of user-given casts: they don't really	msozeau	2008-11-07
*	- Ajout possibilité de lancer ocamldebug sur coqide	herbelin	2008-11-07
*	Suite #11533	notin	2008-11-07
*	Correction du bug #1926	notin	2008-11-07
*	Add some example uses of the new record features in Record.v:	msozeau	2008-11-07
*	Fix a bug in the specialization by unification tactic related to the problems	msozeau	2008-11-07
*	Add the ability to give a specific tactic to solve each obligation in	msozeau	2008-11-07
*	Fix universe problem appearing ConCaT using the existing infrastructure for	msozeau	2008-11-07
*	Cosmetic: no more whitespace at end of lines in extraction files	letouzey	2008-11-06
*	Correction d'un petit bug en cas de redéfintion par l'utilisateur de variabl...	notin	2008-11-06
*	Minor fixes:	msozeau	2008-11-05
*	Port [rewrite] tactics to open terms. Currently no check that evars	msozeau	2008-11-05
*	Fix in the unification algorithm using evars: unify types of evar	msozeau	2008-11-05
*	Move Record desugaring to constrintern and add ability to use notations	msozeau	2008-11-05
*	Suite commit 11539 sur notation Record dans (Co)Inductive (MAJ	herbelin	2008-11-05
*	Petit bug dans le commit précédent.	aspiwack	2008-11-05
*	Nouvelle syntaxe pour écrire des records (co)inductifs :	aspiwack	2008-11-05
*	Better extraction renaming phase (fix #1914 plus other non-reported bugs)	letouzey	2008-11-05
*	Adaptation to ocaml 3.11 new semantics of String.index_from (see bug #1974)	herbelin	2008-11-04
*	2 petites améliorations de coq_makefile (traitement des .ml4 + cibles géné...	notin	2008-11-04
*	Fix CAMLHLIB (due to r11358) (Closes: #1986)	glondu	2008-11-02
*	test-suite/ideal-features/{apply.v -> eapply_evar.v}	glondu	2008-11-02
*	Ajout d'une option -raw pour Coqdoc (sortie en texte brut)	notin	2008-10-31
*	allowed patternidents starting with an '_'	amahboub	2008-10-31
*	The lexer is changer to break former PATTERNIDENT into two tokens.	amahboub	2008-10-30
*	Document native "Declare ML Module"	glondu	2008-10-29
*	Remove calls to Dynlink.add_{interfaces,available_units} altogether	glondu	2008-10-29
*	Adaptation du vieil appel à "apply" sur lemme de symétrie au cas où	herbelin	2008-10-29
*	Oups...	notin	2008-10-29
*	Dépendance des cibles de la documentation envers les cibles de Coq	notin	2008-10-29
*	Native "Declare ML Module" when possible	glondu	2008-10-28
*	petite modif du commit 11513.	soubiran	2008-10-28
*	11511 continued (bug in set.out + incohérence dans "Theorem with"	herbelin	2008-10-28
*	Correction bug 1979.	soubiran	2008-10-28
*	- Fixed many "Theorem with" bugs.	herbelin	2008-10-27
*	Correct enormous bug in interpretation of generalized binders: it simply	msozeau	2008-10-26
*	Fixes and refinements regarding occurrence selection:	herbelin	2008-10-26
*	adding an option Function_raw_tcc to Function	jforest	2008-10-26
*	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