diff options
author | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-12-13 17:33:04 +0100 |
---|---|---|
committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-12-30 19:23:04 +0100 |
commit | bad3f3b784d3de8851615b8f4b7afba734232d8e (patch) | |
tree | be6a12a50d3bf6b73ea7866334585f694370e630 /checker/univ.ml | |
parent | 441bea723c511ed9e18ef005678bd01242b45c49 (diff) |
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.
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 |