coq - The formal proof system

Age	Commit message (Expand)	Author
2001-09-14	Ajout syntaxe "Assert H:T."	herbelin
2001-09-13	eclaircissement du code	courant
2001-09-10	Utilisation d'un type spécifique (elimination_sorts) pour caractériser les ...	herbelin
2001-09-09	Nettoyage reduce_to_ind et one_step_reduce	herbelin
2001-09-09	Préparation à la mise en place d'univers algébriques	herbelin
2001-09-03	Correction d'un bug de pretty-print.	clrenard
2001-08-28	Change la constante d'entree de Immediate	mohring
2001-08-10	Parsing	herbelin
2001-08-08	Renommage TrueCut -> Assert	herbelin
2001-08-08	La grammaire n'était plus LL1	herbelin
2001-08-08	Modification Tauto pour qu'il puisse destructurer des hypotheses de la forme	courant
2001-08-07	Ajout tactique TrueCut qui fait la coupure du calcul des séquents; nouvelle ...	herbelin
2001-08-05	Remplacement de 'clause' par 'hyps' pour les tactiques qui ne peuvent pas s'a...	herbelin
2001-08-05	Elimination des coupures quand les 'clause' se réduisent à des hypothèses,...	herbelin
2001-08-05	Remplacement de 'clause' par 'hyps' pour les tactiques qui ne peuvent pas s'a...	herbelin
2001-08-05	Mise en place d'un nouveau Destruct sur le modèle du nouvel Induction	herbelin
2001-08-05	Suppression des TmpHyp disgracieuses dans Decompose; utilisation de combinate...	herbelin
2001-08-05	Elimination des coupures quand les 'clause' se réduisent à des hypothèses,...	herbelin
2001-08-01	Ajout code pour un Destruct similaire au NewInduction	herbelin
2001-07-13	Branchement de induction/destruct sur intros_until_n (intros_do obsolete ne p...	herbelin
2001-07-10	Branchement sur bad_tactic_args	herbelin
2001-07-10	Branchement sur bad_tactic_args	herbelin
2001-07-10	Ajout du .ml pour la tactique Setoid_replace	clrenard
2001-07-10	Changement de place de la tactique Setoid_rewrite et renommage	clrenard
2001-07-04	ajout Show Intro(s)	letouzey
2001-06-29	Autoriser Apply avec un but sous forme d'implication ou de quantification	barras
2001-06-29	traitement du let dans red_product (tactique Red)	barras
2001-06-27	commit d'un bug de Apply.	barras
2001-06-25	Refine sur les CoFix	filliatr
2001-06-25	Les réduction dans les hypothèses s'appliquent maintenant au corps de la d�...	herbelin
2001-06-25	Découpage de g_tactic.ml4 en 2 (pour satisfaire les contraintes de la compil...	herbelin
2001-06-15	Fix d'un bug de Tauto	delahaye
2001-06-13	Prise en compte env local (et defs locales) dans Change	herbelin
2001-06-01	Correction d'un bug du a un Intros trop violent	delahaye
2001-06-01	Backtrack vers comportement de la V6 pour eviter les globaux dans le nommage ...	herbelin
2001-05-31	Amelioration - subjective - de l'affichage des Hint	herbelin
2001-05-28	Pretty -> Prettyp	filliatr
2001-05-25	Remplacement push_rec_types (Rel) pour Fix parpush_named_rec_types	herbelin
2001-05-23	amelioration des messages d'erreurs vis a vis des evars	barras
2001-05-03	Changement de la structure des points fixes	barras
2001-04-24	Ajout du cas True->A\|-B	delahaye
2001-04-19	Fonction lookup enlevee	delahaye
2001-04-15	Mise en page	herbelin
2001-04-12	Ajout de _ dans les patterns d'intro	mohring
2001-04-12	Mis un message d'erreur explicite pour l'echec de Elim en cas	mohring
2001-04-03	Make it possible to perform proofs by induction even on non-inductive types,	bertot
2001-03-28	amelioration de la structure des univers	barras
2001-03-22	Problèmes de NewInduction	herbelin
2001-03-15	entetes	filliatr
2001-03-09	bug de refine: uncaught exception Array.sub	barras