aboutsummaryrefslogtreecommitdiff
path: root/kernel/genOpcodeFiles.ml
diff options
context:
space:
mode:
authorcoqbot-app[bot]2020-11-15 15:13:46 +0000
committerGitHub2020-11-15 15:13:46 +0000
commite476ded00efed5185a435f28551f1aa88b6c374a (patch)
tree35b093d8d21342cbeb346510be0dcf0b8d0b0438 /kernel/genOpcodeFiles.ml
parenta118b906b3da7cb2e03a72f7a8079a7fc99c6f84 (diff)
parent5c51dc73c236e167a2aaf34d271f737b72d84210 (diff)
Merge PR #13375: Distinguish one_pattern and one_term nonterminals, improve description of Instance command
Reviewed-by: Zimmi48
Diffstat (limited to 'kernel/genOpcodeFiles.ml')
0 files changed, 0 insertions, 0 deletions