coq - The formal proof system

Age	Commit message (Expand)	Author
2002-07-15	Pb de factorisation camlp4	herbelin
2002-07-11	Généralisation des syntaxes ': T := t', ':= t : T', ': T', ':= t' pour	herbelin
2002-06-03	Intgration uniforme de coercions dans les dclarations (Variable and co) et re...	herbelin
2002-05-30	Finalement un seul constr pour l'instant dans ExtraRedExpr	herbelin
2002-05-29	Nouveau modèle d'analyse syntaxique et d'interprétation des tactiques et co...	herbelin
2002-03-17	Meilleure gestion de la reduction dans Field	delahaye
2002-01-18	Plusieurs arguments autorisés pour Require et Read Module	herbelin
2001-12-16	Ajout syntaxe 'Canonical Structure' en remplacement de @Definition + suppress...	herbelin
2001-12-10	- condition de garde (suite)	barras
2001-10-23	Modifs Tacinterp + debugger de tactiques + syntaxe de R + DiscrR	delahaye
2001-10-17	Abstraction de l'immplementation de dirpath et implementation dans l'autre se...	herbelin
2001-10-11	Suppression option immediate_discharge; nettoyage de Declare et conséquences	herbelin
2001-09-20	Transparent	barras
2001-08-10	Parsing	herbelin
2001-07-13	reparation regles pour parsing Coercion Local	mohring
2001-06-11	Fix de quelques bugs syntaxiques de Ltac	delahaye
2001-04-09	Uniformisation des 'Save def_tok id'	herbelin
2001-04-09	nettoyage d'entrees de grammaires inutiles	courant
2001-04-05	mise en place de Correctness; vieille syntaxe Extraction viree de g_vernac.ml4	filliatr
2001-04-04	renommage du module Pcoq.Vernac en Pcoq.Vernac_ pour contourner un bug d'ocam...	filliatr
2001-03-15	entetes	filliatr
2001-02-16	Prise en compte noms longs dans Implicits	herbelin
2001-02-09	Bug point final dans la syntaxe theorem_body	herbelin
2001-02-05	Correction pour Time pour ne pas etre oblige de mettre deux points	delahaye
2001-01-27	Factorisation du '.' final	herbelin
2001-01-24	Prise en compte des noms longs dans les Hints et les Coercions	herbelin
2001-01-24	Ajout de constantes locales dans les Records	herbelin
2000-12-29	Ajout du Let pour le langage de tactiques	delahaye
2000-12-20	ajout ident_or_constrarg pour NewInduction	herbelin
2000-11-21	Begin-End Silent deviennent Set?Unset Silent	mohring
2000-11-20	Prise en compte des noms qualifiés dans certaines commandes	herbelin
2000-11-05	Déplacement d'une partie de g_vernac.ml4 dans g_proofs.ml4 car fichier deven...	herbelin
2000-11-03	compilation des fichiers ml4 sans GNUseries	filliatr
2000-10-30	Priorite du Try/Orelse + Debug switch + correction bug dans Pattern	delahaye
2000-08-17	Pattern matching de sous-termes + exceptions dans le lexer	delahaye
2000-07-26	Ajout syntaxe [ phr1 ... phrn ]. pour grouper des commandes (pour Time ou Gra...	herbelin
2000-06-02	':>' est devenu un seul token	herbelin
2000-05-03	Ajout du langage de tactiques	delahaye
2000-01-20	Bête renommage	herbelin
2000-01-13	Nettoyage des fichiers de parsing	herbelin
2000-01-07	Renommage command en constr	herbelin
1999-12-15	Les inductifs dans Scheme doivent être des ident d'inductifs	herbelin
1999-12-12	modules et coqc	filliatr
1999-12-10	- erreurs Pretype	filliatr
1999-12-10	debug discharge et inductifs	filliatr
1999-12-01	Intégration du Termast et du Retyping de HH, et modifications connexes	herbelin
1999-09-08	compilation des grammaires (ouf)	filliatr
1999-09-08	modules grammaire Coq	filliatr