coq/kernel/make-opcodes, branch master The formal proof system [Kernel] Simpler generation of opcode files 2019-03-01T14:01:23+00:00 Vincent Laporte 2019-02-21T16:45:12+00:00 8541a43c053d659196992f4e990ec317cd199af8 Files kernel/copcodes.ml, kernel/byterun/coq_instruct.h, and kernel/byterun/coq_jumptbl.h are generated by a simple OCaml program rather than a pipeline of sed and awk text processing. 
Files kernel/copcodes.ml, kernel/byterun/coq_instruct.h, and
kernel/byterun/coq_jumptbl.h are generated by a simple OCaml program
rather than a pipeline of sed and awk text processing.
More comments in VM. 2016-10-19T12:49:57+00:00 Maxime Dénès 2016-10-19T12:46:25+00:00 6fbe3c850bac9cbdfa64dbdcca7bd60dc7862190 






COMMITED BYTECODE COMPILER
2004-10-20T13:50:08+00:00

barras

2004-10-20T13:50:08+00:00

9c6487ba87f448daa28158c6e916e3d932c50645

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6245 85f007b7-540e-0410-9357-904b9bb8a0f7





git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6245 85f007b7-540e-0410-9357-904b9bb8a0f7