| Age | Commit message (Expand) | Author |
|---|---|---|
| 2006-02-09 | Minor bugs fixes | bertot |
| 2006-02-08 | One can use a measure {mes f x} instead of a well-founded relation in GenFixp... | bertot |
| 2006-02-08 | Julien: | bertot |
| 2006-02-03 | + Adding an error message when the function cannot be defined | bertot |
| 2006-01-28 | Réorganisation de la structure interne des types de déclarations (decl_kinds) | herbelin |
| 2006-01-21 | Messages de idtac et fail peuvent maintenant être des listes de string, int ... | herbelin |
| 2006-01-18 | Recursive Definition now supports functions with more than one argument. | coq |
| 2006-01-12 | Changing well founded induction to fix on accessibility proof in order | bertot |
| 2006-01-11 | removes several warnings in contrib/interface | bertot |
| 2005-12-26 | Suppression des parseurs et printeurs v7; suppression du traducteur (mcanisme... | herbelin |
| 2005-12-02 | Changement des named_context | gregoire |
| 2005-11-14 | avoids warnings about unused variables | bertot |
| 2005-11-07 | Adds tools to help in defining new general recursive functions | bertot |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |