diff options
| author |  Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2018-05-08 12:59:35 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2018-05-08 12:59:35 +0200 |
| commit | 96a357777e2e3c1273a61e0767bc04085d56835e (patch) | |
| tree | 0903a7e3054db52c81f2b4c6d54812a8cf6a775f /engine/universes.mli | |
| parent | 6c8b00e47334f60f200256d45a5542fa80ce4b12 (diff) | |
Don't use ref universe_opt_subst
Diffstat (limited to 'engine/universes.mli')
| -rw-r--r-- | engine/universes.mli | 9 |
1 files changed, 4 insertions, 5 deletions
diff --git a/engine/universes.mli b/engine/universes.mli index e6bee42bb..df2e961d6 100644 --- a/engine/universes.mli +++ b/engine/universes.mli @@ -184,19 +184,18 @@ val normalize_univ_variables : universe_opt_subst -> val normalize_univ_variable : find:(Level.t -> Universe.t) -> - update:(Level.t -> Universe.t -> Universe.t) -> Level.t -> Universe.t -val normalize_univ_variable_opt_subst : universe_opt_subst ref -> +val normalize_univ_variable_opt_subst : universe_opt_subst -> (Level.t -> Universe.t) -val normalize_univ_variable_subst : universe_subst ref -> +val normalize_univ_variable_subst : universe_subst -> (Level.t -> Universe.t) -val normalize_universe_opt_subst : universe_opt_subst ref -> +val normalize_universe_opt_subst : universe_opt_subst -> (Universe.t -> Universe.t) -val normalize_universe_subst : universe_subst ref -> +val normalize_universe_subst : universe_subst -> (Universe.t -> Universe.t) (** Create a fresh global in the global environment, without side effects. |