1 files changed, 37 insertions, 5 deletions
diff --git a/engine/uState.ml b/engine/uState.ml
index aa7ec63a6f..5747ae2ad4 100644
--- a/engine/uState.ml
+++ b/engine/uState.ml
@@ -101,13 +101,21 @@ let context ctx = Univ.ContextSet.to_context ctx.uctx_local
 
 let const_univ_entry ~poly uctx =
   let open Entries in
-  if poly then Polymorphic_const_entry (context uctx)
+  if poly then
+    let (binders, _) = uctx.uctx_names in
+    let uctx = context uctx in
+    let nas = UnivNames.compute_instance_binders (Univ.UContext.instance uctx) binders in
+    Polymorphic_const_entry (nas, uctx)
   else Monomorphic_const_entry (context_set uctx)
 
 (* does not support cumulativity since you need more info *)
 let ind_univ_entry ~poly uctx =
   let open Entries in
-  if poly then Polymorphic_ind_entry (context uctx)
+  if poly then
+    let (binders, _) = uctx.uctx_names in
+    let uctx = context uctx in
+    let nas = UnivNames.compute_instance_binders (Univ.UContext.instance uctx) binders in
+    Polymorphic_ind_entry (nas, uctx)
   else Monomorphic_ind_entry (context_set uctx)
 
 let of_context_set ctx = { empty with uctx_local = ctx }
@@ -140,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
@@ -394,8 +420,11 @@ let check_univ_decl ~poly uctx decl =
   let ctx =
     let names = decl.univdecl_instance in
     let extensible = decl.univdecl_extensible_instance in
-    if poly
-    then Entries.Polymorphic_const_entry (universe_context ~names ~extensible uctx)
+    if poly then
+      let (binders, _) = uctx.uctx_names in
+      let uctx = universe_context ~names ~extensible uctx in
+      let nas = UnivNames.compute_instance_binders (Univ.UContext.instance uctx) binders in
+      Entries.Polymorphic_const_entry (nas, uctx)
     else
       let () = check_universe_context_set ~names ~extensible uctx in
       Entries.Monomorphic_const_entry uctx.uctx_local
@@ -566,6 +595,9 @@ let make_flexible_variable ctx ~algebraic u =
   {ctx with uctx_univ_variables = uvars'; 
       uctx_univ_algebraic = avars'}
 
+let make_nonalgebraic_variable ctx u =
+  { ctx with uctx_univ_algebraic = Univ.LSet.remove u ctx.uctx_univ_algebraic }
+
 let make_flexible_nonalgebraic ctx =
   {ctx with uctx_univ_algebraic = Univ.LSet.empty}