diff options
| author | Gaëtan Gilbert | 2020-12-02 14:51:13 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2020-12-04 15:33:05 +0100 |
| commit | 40f6ecfaef5976e6955d6468844b782bc88e6280 (patch) | |
| tree | 74d0d98e7cbbf53b0a709c9aad553b6733a68627 /engine | |
| parent | b399887760b1a6f7fcd99c349ed9b46b8a430cb3 (diff) | |
Delay inventing names for monomorphic universes
This avoids doing it repeatedly for nothing in intern/extern.
Diffstat (limited to 'engine')
| -rw-r--r-- | engine/uState.ml | 17 | ||||
| -rw-r--r-- | engine/uState.mli | 2 |
2 files changed, 2 insertions, 17 deletions
diff --git a/engine/uState.ml b/engine/uState.ml index 0eb8475958..20ea24dd87 100644 --- a/engine/uState.ml +++ b/engine/uState.ml @@ -157,23 +157,8 @@ let of_binders names = in { empty with names = (names, rev_map) } -let invent_name (named,cnt) u = - let rec aux i = - let na = Id.of_string ("u"^(string_of_int i)) in - if Id.Map.mem na named then aux (i+1) - else Id.Map.add na u named, i+1 - in - aux cnt - let universe_binders uctx = - let named, rev = uctx.names in - let named, _ = LSet.fold (fun u named -> - match LMap.find u rev with - | exception Not_found -> (* not sure if possible *) invent_name named u - | { uname = None } -> invent_name named u - | { uname = Some _ } -> named) - (ContextSet.levels uctx.local) (named, 0) - in + let named, _ = uctx.names in named let instantiate_variable l b v = diff --git a/engine/uState.mli b/engine/uState.mli index 442c29180c..9cff988c99 100644 --- a/engine/uState.mli +++ b/engine/uState.mli @@ -79,7 +79,7 @@ val univ_entry : poly:bool -> t -> Entries.universes_entry (** Pick from {!context} or {!context_set} based on [poly]. *) val universe_binders : t -> UnivNames.universe_binders -(** Return names of universes, inventing names if needed *) +(** Return local names of universes. *) (** {5 Constraints handling} *) |