diff options
| author | Pierre-Marie Pédrot | 2015-11-17 19:24:41 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2015-11-17 20:00:30 +0100 |
| commit | c4fef5b9d2be739cad030131fd6fc4c07d5e2e08 (patch) | |
| tree | 12ac35787f1c6e4412af3b133b3a3d553938fe38 /kernel/indtypes.ml | |
| parent | af399d81b0505d1f0be8e73cf45044266d5749e5 (diff) | |
More optimizations of [Clenv.clenv_fchain].
Everywhere we know that the universes of the left argument are an
extension of the right argument, we do not have to merge universes.
Diffstat (limited to 'kernel/indtypes.ml')
0 files changed, 0 insertions, 0 deletions