diff options
| author | Matthieu Sozeau | 2014-06-20 14:15:02 +0200 |
|---|---|---|
| committer | Matthieu Sozeau | 2014-06-20 14:15:02 +0200 |
| commit | 1e2fa3a3a0ce3c5be93287ee034fc1fddc82d733 (patch) | |
| tree | 4a75e04b5d54c1a53f49db80fd20c04cec0195ae /kernel/type_errors.ml | |
| parent | cbf1315572bdb86dd5fc9102690f3585194bbc30 (diff) | |
Bug 27 closed now that universe contexts can be refined during the proof,
here instantiating a flexible level with Set.
Diffstat (limited to 'kernel/type_errors.ml')
0 files changed, 0 insertions, 0 deletions