diff options
| author | Théo Zimmermann | 2016-12-16 18:38:20 +0100 |
|---|---|---|
| committer | Théo Zimmermann | 2017-02-07 17:38:00 +0100 |
| commit | 9e87e9582ffe68ff549347d4fab37f7514992361 (patch) | |
| tree | 8c0d636d83a30301045894c2c500f2e29407e0f4 /kernel/nativevalues.ml | |
| parent | 5e909ab948ea3db4b5d734ec1c68198874c9724c (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 'kernel/nativevalues.ml')
0 files changed, 0 insertions, 0 deletions