coq - The formal proof system

Age	Commit message (Expand)	Author
2003-09-13	Deplacement de Declare vers Termops	herbelin
2003-09-12	Déplacement de Declare juste à la fin de interp pour pouvoir accéder à in...	herbelin
2003-09-12	open superflu	herbelin
2003-09-10	Bug predicat old Case	herbelin
2003-09-09	Bug predicat let-tuple	herbelin
2003-09-09	Ajout construction If primitive dans constr_expr et rawconstr	herbelin
2003-09-06	Paramétrisation vis à vis de existential_key	herbelin
2003-09-06	Mise en place possibilité de définitions locales dans les paramètres des i...	herbelin
2003-08-31	V8: FUNCLASS -> Funclass, SORTCLASS -> Sortclass	herbelin
2003-08-12	Bug et améliorations diverses	herbelin
2003-08-12	Bug détypage du fix	herbelin
2003-08-11	Nouvelle mouture du traducteur v7->v8	herbelin
2003-06-11	Pb quand une meme classe est definie dans 2 fichiers	herbelin
2003-06-10	Simplification case_info	herbelin
2003-06-10	Ajout notation c.(f) en v8 pour les projections de Record	herbelin
2003-06-10	Factorisation de detype_case pour utilisation par l'afficheur de pattern	herbelin
2003-06-10	Amélioration afficheur de Cases pour les constr_pattern	herbelin
2003-06-08	Tables logarithmiques pour les coercions + nettoyage	herbelin
2003-05-22	Preservation affichage des ?n en V7	herbelin
2003-05-21	Suppression définitive de lmatch et or_metanum dans tacinterp	herbelin
2003-05-21	Fusion à l'essai de lmatch et lfun dans tacinterp; utilisation de noms pour ...	herbelin
2003-05-19	Renommage CMeta en CPatVar qui sert à saisir les PMeta de Pattern	herbelin
2003-05-13	Rien d'important	herbelin
2003-04-27	Affichage des Fix contenant des Let dans leur context (ce que la tactique Fix...	herbelin
2003-04-16	simplification: fst (list_chop n l) = firstn n l et snd (list_chop n l) = lis...	letouzey
2003-04-07	Globalisation des noms de tactiques dans les définitions de tactiques	herbelin
2003-04-07	Globalisation des noms de tactiques dans les définitions de tactiques	herbelin
2003-04-01	Correction bug #261 + amélioration nommage	herbelin
2003-03-29	Mise en place de 'Implicit Variable' (variante du 'Reserve' de mizar)	herbelin
2003-03-21	* empty log message *	barras
2003-03-12	* empty log message *	barras
2003-02-02	Bug affichage let destructurant	herbelin
2003-02-01	Backtrack sur le filtrage des applications partielles (change Tauto/Intuition)	herbelin
2003-01-31	Ajout d'un filtrage d'application partielle	herbelin
2003-01-31	Unification plus efficace vis à vis du LetIn	herbelin
2003-01-23	reparation des contribs: lors de l'unification, reduire les beta redexes	barras
2003-01-22	modified the unification algorithm to try first order unification before	barras
2003-01-22	ajout de whd_state dans l'interface	barras
2003-01-19	Localisation	herbelin
2003-01-15	Problème de désynchronisation des variables du type et du corps d'un point-...	herbelin
2003-01-15	Bug en présence de let-in	herbelin
2002-12-23	Prise en compte application partielle dans dependent	herbelin
2002-12-21	Légère amélioration des messages d'erreur des with-bindings et des Rewrite	herbelin
2002-12-21	Affinement affichage	herbelin
2002-12-19	Petit netoyage dans lib	coq
2002-12-19	apres correction du probleme de Global.env, retour du mis_constr_nargs_env	letouzey
2002-12-17	ma bidouille marche pas...	letouzey
2002-12-13	correction (temporaire ?) d'un probleme de Printer.prterm_env utilisant quand...	letouzey
2002-12-10	Commentaires	herbelin
2002-12-09	Essai suppression nf_betaiota dans type_of	herbelin