aboutsummaryrefslogtreecommitdiff
path: root/dev/base_include
diff options
context:
space:
mode:
authorcoqbot-app[bot]2020-08-25 15:25:56 +0000
committerGitHub2020-08-25 15:25:56 +0000
commit3365b1e640e9a9a4694c85d3f988115ce79be9f9 (patch)
tree6c344dcc2e968f7b0871f72c3d490ebdbea417d4 /dev/base_include
parentaf5e7d44a2a685fe72a65df3daae577938eaa989 (diff)
parent8e78a6dc20858ce2ca989da903e6311ffe727695 (diff)
Merge PR #12897: [test-suite] close the proof added in #12857
Reviewed-by: Zimmi48
Diffstat (limited to 'dev/base_include')
0 files changed, 0 insertions, 0 deletions