| Age | Commit message (Expand) | Author |
|---|---|---|
| 2000-10-01 | Code mort | herbelin |
| 2000-09-14 | Abstraction de constr | herbelin |
| 2000-09-10 | Correction pour make doc | herbelin |
| 2000-09-10 | Ajout d'un LetIn primitif. | herbelin |
| 2000-07-24 | Passage à des contextes de vars et de rels pouvant contenir des déclarations | herbelin |
| 2000-07-01 | Plus de env et sigma dans get_arity, plus de sigma dans make_arity | herbelin |
| 2000-07-01 | Extension de find_inductive aux co-inductifs et renommage en find_rectype | herbelin |
| 2000-06-03 | Retrait des lam_and_pop and co | herbelin |
| 2000-05-22 | suppression de l'env/sigma dans les fonctions de reduction beta et iota seuls | herbelin |
| 2000-05-18 | bugs | herbelin |
| 2000-05-18 | Nettoyage | herbelin |
| 2000-05-05 | Intégration de leminv | herbelin |
| 2000-05-04 | les erreurs | herbelin |
| 2000-05-03 | Ajout du langage de tactiques | delahaye |
| 2000-04-30 | Intégration progressive | herbelin |
| 2000-03-27 | Inversion (pas termine) | filliatr |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |