aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/ltac
diff options
context:
space:
mode:
authorGravatar Maxime Dénès <mail@maximedenes.fr>2018-05-15 10:31:31 +0200
committerGravatar Maxime Dénès <mail@maximedenes.fr>2018-05-15 10:31:31 +0200
commitcfed57b021b89018d1bb30c6aa0957299fe35d8d (patch)
tree08c656b3146dfca02288ade499de1db2de127f00 /plugins/ltac
parent3a0dfe68e14f8f5e40cc56c3bb0c583318debeb5 (diff)
parentd5a352faa11576d2eda294ca6872d543b0e695da (diff)
Merge PR #7487: Remove duplicate entries for Proof, Qed, Defined, Admitted.
Diffstat (limited to 'plugins/ltac')
0 files changed, 0 insertions, 0 deletions