coq - The formal proof system

Age	Commit message (Expand)	Author
2008-11-09	better fix for #1931 by using sort_of	letouzey
2008-11-09	Oops... forgot to commit a file related to r11561.	msozeau
2008-11-09	Add test-suite file related to discussion of syntax of implicit binders.	msozeau
2008-11-09	More factorization of inductive/record and typeclasses: move class	msozeau
2008-11-09	- Fixed bug 1968 (inversion failing due to a Not_found bug introduced in	herbelin
2008-11-08	Apply vmconv if there are no _undefined_ evars around.	msozeau
2008-11-07	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-06	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-05	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-04	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-02	Fix CAMLHLIB (due to r11358) (Closes: #1986)	glondu
2008-11-02	test-suite/ideal-features/{apply.v -> eapply_evar.v}	glondu
2008-10-31	Ajout d'une option -raw pour Coqdoc (sortie en texte brut)	notin
2008-10-31	allowed patternidents starting with an '_'	amahboub
2008-10-30	The lexer is changer to break former PATTERNIDENT into two tokens.	amahboub
2008-10-29	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-28	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-27	- Fixed many "Theorem with" bugs.	herbelin
2008-10-26	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-25	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-24	Raise informative errors instead of Failures or anomalies in case a meta	msozeau