From bad3f3b784d3de8851615b8f4b7afba734232d8e Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Wed, 13 Dec 2017 17:33:04 +0100 Subject: Moving some universe substitution code out of the kernel. This code was not used at all inside the kernel, it was related to universe unification that happens in the upper layer. It makes more sense to put it somewhere upper. --- checker/univ.ml | 8 -------- checker/univ.mli | 2 -- 2 files changed, 10 deletions(-) (limited to 'checker') 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 diff --git a/checker/univ.mli b/checker/univ.mli index 0eadc6801..21c94d952 100644 --- a/checker/univ.mli +++ b/checker/univ.mli @@ -150,8 +150,6 @@ type universe_level_subst_fn = universe_level -> universe_level type universe_subst = universe universe_map type universe_level_subst = universe_level universe_map -val level_subst_of : universe_subst_fn -> universe_level_subst_fn - (** {6 Universe instances} *) module Instance : -- cgit v1.2.3