coq - The formal proof system

Age	Commit message (Expand)	Author
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
2000-11-05	Déplacement d'une partie de g_vernac.ml4 dans g_proofs.ml4 car fichier deven...	herbelin