| Commit message (Expand) | Author | Age | |
|---|---|---|---|
| * | Ajout d'une heuristique pour les types dependants |  delahaye | 2001-02-05 |
| * | Message d'erreur plus explicite pour Tauto | delahaye | 2001-02-05 |
| * | rétablissement nouveau Tauto |  filliatr | 2001-02-05 |
| * | Résolution d'un bug de simplification | delahaye | 2001-02-03 |
| * | oubli de Closure.EvalConstRef | filliatr | 2001-02-01 |
| * | - coqc : option -image | filliatr | 2001-02-01 |
| * | Bug fixed: the case [ id : ?1 -> ?2 |- ?] was missing in tauto_main |  sacerdot | 2001-01-30 |
| * | As an heuristic, now both in tauto and intuition we try to avoid the initial | sacerdot | 2001-01-29 |
| * | Elimination du ' | delahaye | 2000-11-28 |
| * | Nouveau choix pour l'intros initial | delahaye | 2000-11-24 |
| * | On n'introduit que des produits non dependants | delahaye | 2000-11-23 |
| * | compilation des fichiers ml4 sans GNUseries | filliatr | 2000-11-03 |
| * | Remplacement de Tauto et Intuition | delahaye | 2000-10-30 |
 |
index : coq | |
| the Coq proof assistant |
| aboutsummaryrefslogtreecommitdiffhomepage |