aboutsummaryrefslogtreecommitdiff
path: root/kernel/genOpcodeFiles.ml
diff options
context:
space:
mode:
authorcoqbot-app[bot]2021-01-09 12:34:12 +0000
committerGitHub2021-01-09 12:34:12 +0000
commit723440611965ccdecfd56e61c8f1f8618a08841d (patch)
tree9d3582f11361a788c7f60568fb95d112839eec1e /kernel/genOpcodeFiles.ml
parent7b946aa196490be8790cd5b46d0860b3bf6e33e1 (diff)
parent70d557994583bd081787e28f68d627a0833eb9c0 (diff)
Merge PR #13299: Remember universe instances of constants in notations
Reviewed-by: SkySkimmer Reviewed-by: herbelin
Diffstat (limited to 'kernel/genOpcodeFiles.ml')
0 files changed, 0 insertions, 0 deletions