coq - The formal proof system

Age	Commit message (Expand)	Author
2002-10-29	Mais laisser la syntaxe (!id) aussi disponible !	herbelin
2002-10-29	Parenthèse non obligatoires autour de !id sans argument	herbelin
2002-10-28	Des critères plus fins d'analyse des implicites automatiques; meilleur affic...	herbelin
2002-10-13	Mise en place de 'Scope' pour gérer des ensembles de notations - phase 1; ha...	herbelin
2002-05-29	Nouveau modèle d'analyse syntaxique et d'interprétation des tactiques et co...	herbelin
2002-05-27	Ajout de Eval, Inst et Check	delahaye
2001-11-08	Prise en compte de la syntaxe [x:=c:t]b comme équivalent de [x:=c::t]b	herbelin
2001-08-10	Parsing	herbelin
2001-06-19	Extension des parametres de Clear + Inst	delahaye
2001-06-18	Interpretation MetaId + Progress + Inst	delahaye
2001-06-11	Reparation d'un bug d'affichage. Les let destructurants, if, et vieux Case	clrenard
2001-04-14	Non parenthesage des applications de tactiques	delahaye
2001-03-15	entetes	filliatr
2000-11-20	Acceptation des noms qualifiés; nouveau lexeme METAIDENT pour les $id	herbelin
2000-11-03	compilation des fichiers ml4 sans GNUseries	filliatr
2000-09-10	Suppression de Abst	herbelin
2000-09-10	Ajout d'un LetIn primitif.	herbelin
2000-08-17	Pattern matching de sous-termes + exceptions dans le lexer	delahaye
2000-06-21	- $BINDER -> BINDER dans g_constr.ml4 (=> erreur syntax Fix)	filliatr
2000-05-03	Ajout du langage de tactiques	delahaye
2000-04-28	Déplacement du type reference dans Term	herbelin
2000-03-30	erreurs lexicales dans les patterns (manquait des espaces)	filliatr
2000-01-13	Nettoyage des fichiers de parsing	herbelin
2000-01-07	Renommage command en constr	herbelin