diff options
| author | Matthieu Sozeau | 2015-11-04 14:35:02 -0500 |
|---|---|---|
| committer | Matthieu Sozeau | 2015-11-04 14:35:02 -0500 |
| commit | 209faf81c432c39d4537f8b1dc5c9947d4349d30 (patch) | |
| tree | 597ccf58342b2b00751d5f777caeaaffe051c0b1 /pretyping | |
| parent | acc54398bd244b15d4dbc396836c279eabf3bf6b (diff) | |
Univs: update refman, better printers for universe contexts.
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 }) |