coq - The formal proof system

Age	Commit message (Expand)	Author
2000-10-04	Utilisation de local_strong plutôt que strong buggé avec défs locales (2ème)	herbelin
2000-10-04	Commit malencontreux sur précédente version	herbelin
2000-10-04	Mise en conformité nouveau Simpl pour Fix	herbelin
2000-10-04	Nouvelle stratégie de nommage dans Simpl pour Fix	herbelin
2000-10-04	Utilisation de local_strong plutôt que strong buggé avec défs locales	herbelin
2000-10-04	Code mort	herbelin
2000-10-04	MAJ	herbelin
2000-10-04	Ajout LetIn dans prim_extractor	herbelin
2000-10-04	Nouveau bug dans la réduction de Fix par red_elim_const	herbelin
2000-10-04	Touche finale à la réduction du let in dans conv et closure	herbelin
2000-10-04	Elimination des coupures sur le type constant	herbelin
2000-10-04	code mort	herbelin
2000-10-03	Renommage tactique Let en LetTac	herbelin
2000-10-03	Ajout castedopenconstrarg	herbelin
2000-10-03	Ajout de globpr dans tacpr	herbelin
2000-10-03	MAJ	herbelin
2000-10-03	Ajout castedopenconstrarg; Renommage tactique Let en LetTac	herbelin
2000-10-03	Reorganisation des interp_constr	herbelin
2000-10-03	Rebranchement de la tactique Let	herbelin
2000-10-03	L'argument de Refine est un terme ouvert	herbelin
2000-10-03	mise en page	herbelin
2000-10-01	Renommage AppL en App	herbelin
2000-10-01	Renommage AppL en App	herbelin
2000-10-01	Renommage AppL en App; Suppression cast	herbelin
2000-10-01	whd_castapp_stack va de Term dans Reduction	herbelin
2000-10-01	Suppression de ensure_appl	herbelin
2000-10-01	Bug message erreur	herbelin
2000-10-01	MAJ	herbelin
2000-10-01	Code comateux	herbelin
2000-10-01	Plus de whd_castapp	herbelin
2000-10-01	Chasse aux de-cast inutiles	herbelin
2000-10-01	renommage map_constr_with_named_binders	herbelin
2000-10-01	Plus de whd_castapp	herbelin
2000-10-01	Plus de whd_castapp_stack	herbelin
2000-10-01	renommage map_constr_with_named_binders	herbelin
2000-10-01	Passage de la structure DOPN, DOP2, ... à une structure exprimant directemen...	herbelin
2000-10-01	Disparition du type oper mais nouveau type global_reference	herbelin
2000-10-01	Déplacement 'a reference et binder_kind de Term vers Rawterm	herbelin
2000-10-01	Code mort	herbelin
2000-10-01	Elimination de coupures...	herbelin
2000-09-26	Retrait de whd_ise1_metas	herbelin
2000-09-26	Nettoyage pretyping; ise_resolve_* devient understand_*; Ajout d'une notion d...	herbelin
2000-09-26	MAJ	herbelin
2000-09-18	mise a jour dependances	filliatr
2000-09-15	On laisse les LetIn dans les types des constructeurs et des éliminations	herbelin
2000-09-15	Commentaires	herbelin
2000-09-15	Messages d'erreurs	herbelin
2000-09-15	Expression anglaise	herbelin
2000-09-14	Minor correction for Ocamlweb + doc update	coq
2000-09-14	Bugs parenthèses	herbelin