diff options
author | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2015-11-17 19:24:41 +0100 |
---|---|---|
committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 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