aboutsummaryrefslogtreecommitdiff
path: root/kernel/inductive.ml
diff options
context:
space:
mode:
authorPierre-Marie Pédrot2014-08-04 22:11:06 +0200
committerPierre-Marie Pédrot2014-08-04 22:11:06 +0200
commitf9b33f4bc396eaf60abaaee270b4701fe05d82f4 (patch)
tree0b26e6be2a8cd089add5508f3bf5afa77ad5ef8d /kernel/inductive.ml
parent5bba0c3f300f67f402cd8be1801cbb36e4652265 (diff)
Fixing semantics of Univ.Level.equal.
Diffstat (limited to 'kernel/inductive.ml')
0 files changed, 0 insertions, 0 deletions