diff options
Diffstat (limited to 'checker/univ.ml')
| -rw-r--r-- | checker/univ.ml | 8 |
1 files changed, 0 insertions, 8 deletions
diff --git a/checker/univ.ml b/checker/univ.ml index 4f3131813..7d01657df 100644 --- a/checker/univ.ml +++ b/checker/univ.ml @@ -881,14 +881,6 @@ type universe_level_subst = universe_level universe_map (** A full substitution might involve algebraic universes *) type universe_subst = universe universe_map -let level_subst_of f = - fun l -> - try let u = f l in - match Universe.level u with - | None -> l - | Some l -> l - with Not_found -> l - module Instance : sig type t = Level.t array |