aboutsummaryrefslogtreecommitdiff
path: root/plugins/ltac
diff options
context:
space:
mode:
authorMaxime Dénès2017-12-05 12:56:11 +0100
committerMaxime Dénès2017-12-05 12:56:11 +0100
commit2c5e81e3bc6ec17d253aeedd1b2bf4ccd3b81933 (patch)
tree1e8d3db28d8d19b575e9e555f6ce379960c842c1 /plugins/ltac
parentd403b2200ef32afd1eb1087a1f0ef2e6b8bb93f6 (diff)
parent17b620f8bdf47a744d24513dcaef720d9160d443 (diff)
Merge PR #890: Global universe declarations
Diffstat (limited to 'plugins/ltac')
0 files changed, 0 insertions, 0 deletions