Commit message (Collapse) | Author | Age | |
---|---|---|---|
* | changement des _sym par _comm dans setoid_ring | 2006-10-27 | |
| | | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9299 85f007b7-540e-0410-9357-904b9bb8a0f7 | ||
* | - Ajout d'un cast vm dans la syntaxe : x <: t | 2006-07-22 | |
| | | | | | | | | | | | | | | | | | | | Part contre ces cas sont detruis dans les "Definition" (pas dans les "Lemma") je comprends pas ou ils sont enlev'e... Si une id'ee ... - Correction d'un bug dans vm_compute plusieurs fois signal'e par Roland. - Meilleur compilation des coinductifs, on utilise maintenant vraimment du lazy. - Enfin un peu plus de doc dans le code de la vm. Benjamin git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9058 85f007b7-540e-0410-9357-904b9bb8a0f7 | ||
* | COMMITED BYTECODE COMPILER | 2004-10-20 | |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6245 85f007b7-540e-0410-9357-904b9bb8a0f7 |