diff options
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/evd.ml | 5 | ||||
| -rw-r--r-- | pretyping/pretyping.ml | 2 |
2 files changed, 3 insertions, 4 deletions
diff --git a/pretyping/evd.ml b/pretyping/evd.ml index 82c068be07..4a9466f4f3 100644 --- a/pretyping/evd.ml +++ b/pretyping/evd.ml @@ -280,9 +280,8 @@ type evar_universe_context = uctx_univ_variables : Universes.universe_opt_subst; (** The local universes that are unification variables *) uctx_univ_algebraic : Univ.universe_set; - (** The subset of unification variables that - can be instantiated with algebraic universes as they appear in types - and universe instances only. *) + (** The subset of unification variables that can be instantiated with + algebraic universes as they appear in inferred types only. *) uctx_universes : Univ.universes; (** The current graph extended with the local constraints *) uctx_initial_universes : Univ.universes; (** The graph at the creation of the evar_map *) } diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index d484df69c1..d354a6c3c4 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -118,7 +118,7 @@ let _ = { optsync = true; optdepr = false; optname = "minimization to Set"; - optkey = ["Universe";"set";"Minimization"]; + optkey = ["Universe";"Minimization";"ToSet"]; optread = Universes.is_set_minimization; optwrite = (:=) Universes.set_minimization }) |