diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-07-13 00:50:02 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-07-14 13:00:41 +0200 |
| commit | 6806059f7c043b45e6c42f382f069f8c49ed1c1f (patch) | |
| tree | 32e020671754f9606288623e6df543cecb90ac10 /library/global.mli | |
| parent | 0411c7e08b58edc4785c2be396fad0a037056a11 (diff) | |
Getting rid of abstraction breaking code in tclABSTRACT.
This is probably the hardest case of them all, because tclABSTRACT fundamentally
relies on the names of universes from the constant instance being the same as
the one in the current goal. Adding to that the fact that the kernel is doing
strange things when provided with a polymorphic definition with body universe
constraints, it turns out to be a hellish nightmare to handle properly.
At some point we need to clarifiy this in the kernel as well, although we
leave it for some other patch.
Diffstat (limited to 'library/global.mli')
0 files changed, 0 insertions, 0 deletions