diff options
Diffstat (limited to 'kernel/univ.ml')
| -rw-r--r-- | kernel/univ.ml | 4 |
1 files changed, 0 insertions, 4 deletions
diff --git a/kernel/univ.ml b/kernel/univ.ml index 09f884ecd..afe9cbe8d 100644 --- a/kernel/univ.ml +++ b/kernel/univ.ml @@ -440,10 +440,6 @@ struct let set = make Level.set let type1 = hcons (Level.set, 1) - let is_prop = function - | (l,0) -> Level.is_prop l - | _ -> false - let is_small = function | (l,0) -> Level.is_small l | _ -> false |