diff options
| author | Arnaud Spiwack | 2014-08-06 15:27:28 +0200 |
|---|---|---|
| committer | Arnaud Spiwack | 2014-08-06 15:27:28 +0200 |
| commit | 039c0451aa06825451858e580c8c3757d4ff4c2c (patch) | |
| tree | de2540e1d479be1cc5e539c4217e44238072a176 /kernel/inductive.ml | |
| parent | 31e780a275af0ad4be10a61b0096b8f5be38b6d3 (diff) | |
Revert the change in Constrintern introduced by "Add a type of untyped term to Ltac's value."
It was commit 52247f50fa9aed83cc4a9a714b6b8f779479fd9b.
The closure in uconstr renders these changes (pertaining to substitution of ltac variables during internalisation) obsolete.
Diffstat (limited to 'kernel/inductive.ml')
0 files changed, 0 insertions, 0 deletions