diff options
| -rw-r--r-- | engine/uState.ml | 20 | ||||
| -rw-r--r-- | test-suite/output/UnivBinders.out | 4 |
2 files changed, 21 insertions, 3 deletions
diff --git a/engine/uState.ml b/engine/uState.ml index 41905feab7..15bd0335f4 100644 --- a/engine/uState.ml +++ b/engine/uState.ml @@ -148,7 +148,25 @@ let of_binders b = in { ctx with uctx_names = b, rmap } -let universe_binders ctx = fst ctx.uctx_names +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 ctx = + let open Univ in + let named, rev = ctx.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 ctx.uctx_local) (named, 0) + in + named let instantiate_variable l b v = try v := Univ.LMap.set l (Some b) !v diff --git a/test-suite/output/UnivBinders.out b/test-suite/output/UnivBinders.out index 2501ce4f26..d63b6dbfce 100644 --- a/test-suite/output/UnivBinders.out +++ b/test-suite/output/UnivBinders.out @@ -191,12 +191,12 @@ Type@{UnivBinders.57} -> Type@{i} axbar is universe polymorphic Argument scope is [type_scope] Expands to: Constant UnivBinders.axbar -axfoo' : Type@{UnivBinders.59} -> Type@{axbar'.i} +axfoo' : Type@{axbar'.u0} -> Type@{axbar'.i} axfoo' is not universe polymorphic Argument scope is [type_scope] Expands to: Constant UnivBinders.axfoo' -axbar' : Type@{UnivBinders.59} -> Type@{axbar'.i} +axbar' : Type@{axbar'.u0} -> Type@{axbar'.i} axbar' is not universe polymorphic Argument scope is [type_scope] |