aboutsummaryrefslogtreecommitdiff
path: root/Makefile.dev
diff options
context:
space:
mode:
authorcoqbot-app[bot]2020-10-01 18:10:45 +0000
committerGitHub2020-10-01 18:10:45 +0000
commit42a5e337c7a33bf0ec9530b6ce161a3053362b3d (patch)
treeaa5beea45ab81152683bc6a63baf627dc56e0394 /Makefile.dev
parent2855edead8813e48618041e21a467e83019b470d (diff)
parentd6fcf088d556d919b31530eee44bfd3ce1d8919e (diff)
Merge PR #13108: Getting rid of temerarious EConstr.to_constr in Himsg
Reviewed-by: ejgallego
Diffstat (limited to 'Makefile.dev')
0 files changed, 0 insertions, 0 deletions