diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-07-10 17:07:29 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-07-10 17:15:51 +0200 |
| commit | ed3973dfe99899a23d4d6166168972b4a9ce798a (patch) | |
| tree | 92e1ef378876330a065da47f394ef29cdb10a532 /checker/term.mli | |
| parent | 307f08d2ad2aca5d48441394342af4615810d0c7 (diff) | |
Removing a redundant universe instance information in native compute.
Global declarations used to carry universe instances with them, but it
turns out this information is not used anywhere. Instead, instances were
already properly encoded as the first argument of polymorphic definitions.
Diffstat (limited to 'checker/term.mli')
0 files changed, 0 insertions, 0 deletions