coq - The formal proof system

Age	Commit message (Expand)	Author
2005-01-03	Renommage symbols.ml{,i} en notation.ml{,i} pour permettre le chargement de p...	herbelin
2004-12-25	Passage d'une bibliothèque de grands entiers naturels vers une bibliothèque...	herbelin
2004-07-16	Nouvelle en-tête	herbelin
2004-03-27	Export compute_arguments_scope pour utilisation local a la construction des i...	herbelin
2004-03-17	Mise en place de motifs récursifs dans Notation; quelques simplifications au...	herbelin
2004-02-12	Localisation erreur interp_notation	herbelin
2004-01-21	Export information des references de notations pour coqdoc	herbelin
2003-11-22	Traitement plus clair, notamment pour Locate, de quand quoter les composantes...	herbelin
2003-11-12	Test de la reference principale plutot que le module dans lequel se trouve la...	herbelin
2003-11-01	Ajout notations pour motifs de Cases; renommage map_aconstr_with_binders_loc	herbelin
2003-10-28	Ajout de Print Visibility	herbelin
2003-09-30	Ajout 'Close Scope'.	herbelin
2003-09-26	Decouplage printing en v8 pour les interpretations de notations	herbelin
2003-09-21	Changement de la politique de V8only: V8only tout seul signifie	herbelin
2003-09-19	parsing	herbelin
2003-09-12	Activation déclaration automatique de scope d'arguments; affichage scopes d'...	herbelin
2003-06-10	Extension de Locate sur les symboles avec recherche de sous-chaînes; mise en...	herbelin
2003-04-29	Prise en compte des syntaxes v8 dans Uninterpreted Notation	herbelin
2003-04-17	Ajout "at next level" dans Notation	herbelin
2003-04-08	Ajout option "Local" à "Open Scope"	herbelin
2002-12-15	Prise en compte des scopes traversés dans les notations	herbelin
2002-12-03	Préparation à la prise en compte des changements de scopes internes aux not...	herbelin
2002-11-26	Réaffichage des Syntactic Definition (printer constr_expr).	herbelin
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