coq - The formal proof system

Age	Commit message (Expand)	Author
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