aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping/evardefine.ml
diff options
context:
space:
mode:
authorGravatar Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr>2018-04-14 00:28:12 +0200
committerGravatar Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr>2018-04-14 00:28:12 +0200
commitc6369bb7a5a4564d6fd77a2c04c24a1795e95bf9 (patch)
tree85c9dfb0c2d456fb53c1ab50ae91775a96e7e89b /pretyping/evardefine.ml
parentf3b84cf63c242623bdcccd30c536e55983971da5 (diff)
Add missing CHANGES entry for #6169.
Fixes #7243.
Diffstat (limited to 'pretyping/evardefine.ml')
0 files changed, 0 insertions, 0 deletions