coq - The formal proof system

Age	Commit message (Expand)	Author
2001-11-06	Suite de la suppression : enamed_declaration est remplace par evar_map.	clrenard
2001-11-05	GROS COMMIT:	barras
2001-10-23	Modifs Tacinterp + debugger de tactiques + syntaxe de R + DiscrR	delahaye
2001-10-17	Abstraction de l'immplementation de dirpath et implementation dans l'autre se...	herbelin
2001-10-11	Suppression option immediate_discharge; nettoyage de Declare et consÃ©quences	herbelin
2001-10-09	Suppression des arguments sur les constantes, inductifs et constructeurs	barras
2001-10-02	Ajout de dynamiques pour les quotations constr et tactic	delahaye
2001-09-30	Ajout du printer de tactiques + modif du Dynamic ocaml	delahaye
2001-09-24	Changement du message d'erreur pour l'interpreteur de tactiques	delahaye
2001-09-21	Correction due au changement de semantique de Match	delahaye
2001-09-20	Transparent	barras
2001-08-10	Parsing	herbelin
2001-07-19	Changements dans le traitement des qualid's	delahaye
2001-07-02	Evar et Zeta ne sont plus implicites dans Delta (mais le restent dans Compute...	herbelin
2001-07-02	Nettoyage/restructuration des ensembles d'indicateurs de rÃ©ductions	herbelin
2001-06-29	Backtracking pour le Match	delahaye
2001-06-25	Les rÃ©duction dans les hypothÃ¨ses s'appliquent maintenant au corps de la dÃ...	herbelin
2001-06-19	Extension des parametres de Clear + Inst	delahaye
2001-06-18	Interpretation MetaId + Progress + Inst	delahaye
2001-05-07	quelques bug reports mineurs	barras
2001-04-19	Metas dans les Unfold's	delahaye
2001-04-12	Ajout de _ dans les patterns d'intro	mohring
2001-04-03	utilisation de Options.if_verbose	filliatr
2001-03-28	amelioration de la structure des univers	barras
2001-03-15	entetes	filliatr
2001-03-01	DÃ©placement de qualid dans Nametab, hors du noyau	herbelin
2001-02-16	ident au lieu de string pour le nom de base de qualid	herbelin
2001-02-07	Reparation du pretty-print pour les tactiques	delahaye
2001-02-06	Correction pour les Unfold/Fold dans Cbv	delahaye
2001-01-31	Mise en place de la possibilite d'unfolder des variables locales et des const...	filliatr
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-12-19	Correction pour les variables abstraites dans les Tactic Definitions	delahaye
2000-12-02	Portage d'AutoRewrite	delahaye
2000-11-28	Elimination du '	delahaye
2000-11-27	Ajout de evaluable_named_decl et evaluable_rel_decl en parallele au evaluable...	herbelin
2000-11-24	certains effets disparaissent a la sortie des sections, d'autres non (selon S...	filliatr
2000-11-23	Correction d'un bug lorsque des Variables sont clearees dans le but courant	delahaye
2000-11-22	Abstraction du type 'qualid' pour les noms qualifiÃ©s relatifs distinct de 's...	herbelin
2000-11-21	Tout est deja traite dans Tacinterp	delahaye
2000-11-21	Traitement du pretty-print des Redexp	delahaye
2000-11-20	Prise en compte noms longs	herbelin
2000-11-15	methode export	filliatr
2000-11-10	Bugs lies a la confusion load/open et a un open abusivement recursif dans lib...	herbelin
2000-11-07	Modification de la table des tactic Definitions pour eviter l'ecriture	mohring
2000-11-02	suppression des (* open Generic *)	filliatr
2000-10-30	Tactiques utilisateur + debugger	delahaye
2000-10-28	Clarification message d'erreur	herbelin
2000-10-18	Renommage canonique :	herbelin