diff options
| author | Vincent Laporte | 2019-02-21 16:45:12 +0000 |
|---|---|---|
| committer | Vincent Laporte | 2019-03-01 14:01:23 +0000 |
| commit | 8541a43c053d659196992f4e990ec317cd199af8 (patch) | |
| tree | 6ea182cefc82d7a2d8edeaad6d61a152b85b4121 /kernel/type_errors.mli | |
| parent | 9e858cae7d40459142409e793133eb939a0ffc47 (diff) | |
[Kernel] Simpler generation of opcode files
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.
Diffstat (limited to 'kernel/type_errors.mli')
0 files changed, 0 insertions, 0 deletions