diff options
| author | Pierre-Marie Pédrot | 2021-04-07 13:05:46 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2021-04-07 13:05:46 +0200 |
| commit | d98faea005d32b64252bf6bd50eb01f320a2bc8c (patch) | |
| tree | 477a765de071d2c207dbeef2bb1ded17d35800fa /engine/univProblem.mli | |
| parent | 4e802522481684c1c70283cc6975cfaf4d9ceecd (diff) | |
| parent | e7c29762b995827288f09f7ad736185fb090d39c (diff) | |
Merge PR #14078: Remove unused UnivProblem.Set.subst_univs
Reviewed-by: ppedrot
Diffstat (limited to 'engine/univProblem.mli')
| -rw-r--r-- | engine/univProblem.mli | 2 |
1 files changed, 0 insertions, 2 deletions
diff --git a/engine/univProblem.mli b/engine/univProblem.mli index 575f5ac847..6c7a11f529 100644 --- a/engine/univProblem.mli +++ b/engine/univProblem.mli @@ -32,8 +32,6 @@ module Set : sig include Set.S with type elt = t val pr : t -> Pp.t - - val subst_univs : universe_subst_fn -> t -> t end type 'a accumulator = Set.t -> 'a -> 'a option |