aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/ltac
diff options
context:
space:
mode:
authorGravatar Enrico Tassi <Enrico.Tassi@inria.fr>2018-07-20 10:56:08 +0200
committerGravatar Enrico Tassi <Enrico.Tassi@inria.fr>2018-07-20 10:56:08 +0200
commit2de309b65b379a3c496752aa25f1cfc177644222 (patch)
tree2808a0a0a7ce02805488c3d936567ea30d90eaa0 /plugins/ltac
parent161910e3cd7726751ca545262ef8f9c7a69b2a3c (diff)
parentd308a3ad11f38ce3d504a3d29f9894affdd1fbcc (diff)
Merge PR #8089: Remove declare_object for SsrHave NoTCResolution.
Diffstat (limited to 'plugins/ltac')
0 files changed, 0 insertions, 0 deletions