coq - The formal proof system

Age	Commit message (Expand)	Author
2009-10-26	New cleaning phase of the Local/Global option management	herbelin
2009-09-17	Delete trailing whitespaces in all .{v,ml} files	glondu
2009-05-09	- Adding "Hint Resolve ->" and "Hint Resolve <-" for declaration of equivalence	herbelin
2009-01-14	Fixing/improving management of uniform prefix Local and Global	herbelin
2009-01-13	- Standardized prefix use of "Local"/"Global" modifiers as decided in	herbelin
2008-09-14	Add user syntax for creating hint databases [Create HintDb foo	msozeau
2008-09-07	Add the ability to declare [Hint Extern]'s with no pattern.	msozeau
2008-09-07	Fixes in typeclasses resolution. Avoid reducing instances types before	msozeau
2008-03-06	Syntax changes in typeclasses, remove "?" for usual implicit arguments	msozeau
2008-02-22	Merge with lmamane's private branch:	lmamane
2007-07-16	Generalized CAMLP4USE for pp dependencies	corbinea
2007-03-19	Add a parameter to QuestionMark evar kind to say it can be turned into an obl...	msozeau
2006-09-20	Declarative Proof Language: main commit	corbinea
2006-05-29	The "clean integration of subtac" patch.	msozeau
2006-01-28	Suppression code pour hints nommés à la V7 (voire à la V6...)	herbelin
2006-01-21	Messages de idtac et fail peuvent maintenant être des listes de string, int ...	herbelin
2005-12-26	Renommage des Ppnew en Pp (et déplacement dans parsing); renommage des G_*...	herbelin
2004-07-16	Nouvelle en-tête	herbelin
2004-01-02	meilleure presentation des commentaires du traducteur	barras
2003-11-12	Idtac peut prendre un argument à afficher	narboux
2003-10-22	reorganisation des niveaux (ex: = est a 70)	barras
2003-10-08	Mise en place d'un couple 'Conjecture/Admitted' pour déclarer un énoncé in...	herbelin
2003-10-07	Debranchement de l'affichage automatique de Proof par le traducteur (trop com...	herbelin
2003-09-12	Un seul binaire commun v7 et v8 avec détection précoce de l'option -v8 et c...	herbelin
2003-08-11	Nouvelle mouture du traducteur v7->v8	herbelin
2003-06-14	Ajout option Local à Hint, Hints et HintDestruct	herbelin
2003-06-10	Ajout notation c.(f) en v8 pour les projections de Record	herbelin
2003-04-07	Utilisation de CAppExpl au lieu de CRef pour les hints pour qu'aucun implicite	herbelin
2003-03-12	* empty log message *	barras
2002-12-12	Ajout du vernac Proof with	gregoire
2002-11-24	Utilisation des niveaux de camlp4 pour gérer les niveaux de constr; amélior...	herbelin
2002-11-14	Réforme de l'interprétation des termes :	herbelin
2002-07-11	Généralisation des syntaxes ': T := t', ':= t : T', ': T', ':= t' pour	herbelin
2002-06-05	Fusion entre la nouvelle et l'ancienne syntaxe de HintDestruct	herbelin
2002-05-29	Nouveau modèle d'analyse syntaxique et d'interprétation des tactiques et co...	herbelin
2001-12-13	compat ocaml 3.03	filliatr
2001-11-23	Retablissement de la commande Existential que j'avais supprime par erreur.	clrenard
2001-11-19	Diverses petites simplications de la machine de preuves.	clrenard
2001-09-13	Prise en compte qualid dans Hint Unfold	herbelin
2001-07-04	ajout Show Intro(s)	letouzey
2001-06-11	Fix de quelques bugs syntaxiques de Ltac	delahaye
2001-04-09	Uniformisation des 'Save def_tok id'	herbelin
2001-04-04	renommage du module Pcoq.Vernac en Pcoq.Vernac_ pour contourner un bug d'ocam...	filliatr
2001-03-15	entetes	filliatr
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-09	Meta Definition + Tactic Definition	delahaye
2001-01-05	Arite cachee de Match Context + Meta Definition	delahaye
2000-12-29	Ajout du Let pour le langage de tactiques	delahaye
2000-11-05	Nouveau mode de compilation de .ml4	herbelin