coq - The formal proof system

Age	Commit message (Expand)	Author
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-03	Rebranchement de la tactique Let	herbelin
2000-10-01	Renommage AppL en App	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	Code comateux	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-09-26	Retrait de whd_ise1_metas	herbelin
2000-09-15	On laisse les LetIn dans les types des constructeurs et des éliminations	herbelin
2000-09-15	Commentaires	herbelin
2000-09-14	Minor correction for Ocamlweb + doc update	coq
2000-09-14	Abstraction de constr	herbelin
2000-09-14	Nouvelle version de frterm; ajout des contextes dans l'enviornnement de rédu...	herbelin
2000-09-14	Rendus obsolètes par le LetIn	herbelin
2000-09-14	Abstraction de constr	herbelin
2000-09-12	Modification mkAppL; abstraction via kind_of_term; changement dans Reduction	herbelin
2000-09-12	Vers la paramétrisation des fonctions de Reduction et vers la fusion de	herbelin
2000-09-10	nettoyage	herbelin
2000-09-10	Correction pour make doc	herbelin
2000-09-10	Suppression de Abst	herbelin
2000-09-10	Ajout d'un LetIn primitif.	herbelin
2000-09-10	Intégration à Term	herbelin
2000-09-06	Canonisation de certains noms dans Pretyping, Asterm et Safe_typing	herbelin
2000-09-06	Ajout erreur unexpected type	herbelin
2000-09-06	kernel/type_errors.ml	herbelin
2000-08-17	Pattern matching de sous-termes	delahaye
2000-07-25	retablissement make doc et make minicoq	filliatr
2000-07-24	Passage à des contextes de vars et de rels pouvant contenir des déclarations	herbelin
2000-07-21	retablissement minicoq (pour Jacek)	filliatr
2000-07-19	Quelques (i) pour ne pas casser oczmlweb	coq
2000-07-01	Plus de env et sigma dans get_arity, plus de sigma dans make_arity	herbelin
2000-07-01	Précalcul de la forme canonique des constructeurs et arités pour traiter le...	herbelin
2000-07-01	Ajout fonctions sur les arités	herbelin
2000-07-01	Précalcul de la forme canonique des constructeurs et arités pour traiter le...	herbelin
2000-07-01	Extension de find_inductive aux co-inductifs et renommage en find_rectype	herbelin
2000-06-29	Relative prend sigma en plus pour la normalisation du message d'erreur	herbelin
2000-06-29	Broutilles	herbelin
2000-06-29	Ajout make_typed_lazy	herbelin
2000-06-29	Normalisation des Evar avant génération des erreurs	herbelin
2000-06-21	bug discharge STRUCTURE; FrozenState supprimmes dans les ClosedSection -> .vo...	filliatr
2000-06-09	Doc	herbelin
2000-06-03	Divers	herbelin
2000-06-03	Retrait des lam_and_pop and co; ajout d'un destructeur 'lispien' de constr	herbelin
2000-06-02	Retrait de decomp_prod non conforme à sa spec	herbelin
2000-06-02	Retrait de certains casts	herbelin
2000-06-02	doc	herbelin
2000-06-02	Bug DLAM dans strong	herbelin