aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/ltac
diff options
context:
space:
mode:
authorGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2018-04-11 08:33:37 +0200
committerGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2018-04-11 08:33:37 +0200
commit357c94b3e42d4422e311799771f9e28249fc3608 (patch)
treeb9cbefb89a1e27d1f90edd378995f2527d3db054 /plugins/ltac
parent306b45f889f83846b1ab10d3b37d9f3e7817a5db (diff)
Adding an overlay for Ltac2.
Diffstat (limited to 'plugins/ltac')
0 files changed, 0 insertions, 0 deletions