| Commit message (Expand) | Author | Age | |
|---|---|---|---|
| * | Ré-introduction des implicites à la volée dans la définition des inductifs |  herbelin | 2001-01-27 |
| * | syntaxe AST Inversion + commentaires ocamlweb autour de $ |  filliatr | 2000-12-12 |
| * | implicites manuels | filliatr | 2000-11-21 |
| * | separation calcul des implicites et declaration des constantes / inductifs / ... | filliatr | 2000-11-21 |
| * | Ajout implicits_of_global + accès par noms longs | herbelin | 2000-11-20 |
| * | L'état implicite des définitions survivant au discharge redevient celui du ... | herbelin | 2000-10-23 |
| * | suppression de Fw pour les implicites | herbelin | 2000-05-03 |
| * | modifs pour premiere edition de liens | filliatr | 1999-12-02 |
| * | Intégration du Termast et du Retyping de HH, et modifications connexes | herbelin | 1999-12-01 |
| * | poursuite de Vernacentries | filliatr | 1999-12-01 |
| * | module Termast | filliatr | 1999-11-26 |
| * | - un effort sur la doc (ocamlweb) | filliatr | 1999-09-19 |
 |
index : coq | |
| the Coq proof assistant |
| aboutsummaryrefslogtreecommitdiffhomepage |