Commit message (Collapse) | Author | Age | |
---|---|---|---|
* | - Ajout d'un cast vm dans la syntaxe : x <: t | bgregoir | 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 | ||
* | Découpage des printers pour ne pas avoir de dépendances en la vm dans les ↵ | herbelin | 2005-01-02 |
printers de ocamldebug git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6545 85f007b7-540e-0410-9357-904b9bb8a0f7 |