Commit message (Expand) | Author | Age | |
---|---|---|---|
* | Extension syntaxique de rewrite in: au lieu de pouvoir faire | 2006-05-02 | |
* | - Réintroduction d'un parseur de pattern (q_constr.ml4) à usage de | 2006-03-22 | |
* | Ajout option 'using lemmas' à auto/trivial/eauto | 2006-01-28 | |
* | Suppression des parseurs et printeurs v7; suppression du traducteur (mécanis... | 2005-12-26 | |
* | Types inductifs parametriques | 2005-11-02 | |
* | Nouvelle en-tête | 2004-07-16 | |
* | Restructuration des procédures de filtrage | 2003-05-19 | |
* | simplification: fst (list_chop n l) = firstn n l et snd (list_chop n l) = lis... | 2003-04-16 | |
* | Globalisation des noms de tactiques dans les définitions de tactiques | 2003-04-07 | |
* | Repercussion de la possibilit de mettre des hyps quantifiees dans Simplify_eq... | 2002-06-05 | |
* | Rpercussion de la possibilit de mettre des hyps quantifies dans Simplify_eq e... | 2002-06-05 | |
* | Fichiers tactics/*.ml4 remplacent les tactics/*.v | 2002-05-29 |