aboutsummaryrefslogtreecommitdiff
path: root/kernel/cbytegen.ml
AgeCommit message (Collapse)Author
2005-12-02Changement des named_contextgregoire
Ajout de cast indiquant au kernel la strategie a suivre Resolution du bug sur les coinductifs git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7639 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-11-02Types inductifs parametriquesmohring
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7493 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-08-19Sur le conseil de X.Leroy: x=[||] devient Array.length x=0letouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7305 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-11-22compatibility with POWERPCgregoire
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6338 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-11-17bug module M:=N avec vmbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6321 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-11-12Changement dans les boxed values .gregoire
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6295 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-10-20COMMITED BYTECODE COMPILERbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6245 85f007b7-540e-0410-9357-904b9bb8a0f7