aboutsummaryrefslogtreecommitdiff
path: root/dev
diff options
context:
space:
mode:
authorThéo Zimmermann2016-12-16 18:38:20 +0100
committerThéo Zimmermann2017-02-07 17:38:00 +0100
commit9e87e9582ffe68ff549347d4fab37f7514992361 (patch)
tree8c0d636d83a30301045894c2c500f2e29407e0f4 /dev
parent5e909ab948ea3db4b5d734ec1c68198874c9724c (diff)
Remove hackish autounfoldify now that hintdb can be bound to Ltac variables.
It will be possible to replace any call to 'autounfoldify x' with 'autounfold with x'.
Diffstat (limited to 'dev')
0 files changed, 0 insertions, 0 deletions