diff options
| author | Pierre-Marie Pédrot | 2014-09-04 12:09:55 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2014-09-04 12:57:33 +0200 |
| commit | a8a0cd9d5cf849be3b995ffc19e2cb4a0ff33d7a (patch) | |
| tree | 30ef0390ec873bb50914f3196e9af74d48cb5719 /kernel/typeops.ml | |
| parent | ba9ba59be9534b42ede74adfcbf8b85b876590c7 (diff) | |
Revert "Ltac's idtac is now implemented using the new API."
This reverts commit 5b92ff7b0a641bf2daa31b60bf49b57a5d1e8452.
Diffstat (limited to 'kernel/typeops.ml')
0 files changed, 0 insertions, 0 deletions