diff options
| author | Maxime Dénès | 2018-01-08 12:46:22 +0100 |
|---|---|---|
| committer | Maxime Dénès | 2018-01-08 12:46:22 +0100 |
| commit | 47f47713e551f8de18cf2d847f47c1f55b016c8b (patch) | |
| tree | fba8437d2bab7f202181c83a935ff24e865dcc69 /checker | |
| parent | c34744837dae427ac6cb12f5ada198862d8e1e4f (diff) | |
| parent | 4131f060ac42f121685817fcc9546c3899c09ab7 (diff) | |
Merge PR #6425: Cleanup universes in the kernel
Diffstat (limited to 'checker')
| -rw-r--r-- | checker/univ.ml | 8 | ||||
| -rw-r--r-- | checker/univ.mli | 2 |
2 files changed, 0 insertions, 10 deletions
diff --git a/checker/univ.ml b/checker/univ.ml index 4f31318132..7d01657df7 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 0eadc6801f..21c94d9529 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 : |