diff options
Diffstat (limited to 'engine/uState.ml')
| -rw-r--r-- | engine/uState.ml | 12 |
1 files changed, 10 insertions, 2 deletions
diff --git a/engine/uState.ml b/engine/uState.ml index 25d7638686..d4cb59da26 100644 --- a/engine/uState.ml +++ b/engine/uState.ml @@ -114,12 +114,20 @@ let constraints ctx = snd ctx.local let context ctx = ContextSet.to_context ctx.local +let compute_instance_binders inst ubinders = + let revmap = Id.Map.fold (fun id lvl accu -> LMap.add lvl id accu) ubinders LMap.empty in + let map lvl = + try Name (LMap.find lvl revmap) + with Not_found -> Anonymous + in + Array.map map (Instance.to_array inst) + let univ_entry ~poly uctx = let open Entries in if poly then let (binders, _) = uctx.names in let uctx = context uctx in - let nas = UnivNames.compute_instance_binders (UContext.instance uctx) binders in + let nas = compute_instance_binders (UContext.instance uctx) binders in Polymorphic_entry (nas, uctx) else Monomorphic_entry (context_set uctx) @@ -433,7 +441,7 @@ let check_univ_decl ~poly uctx decl = if poly then let (binders, _) = uctx.names in let uctx = universe_context ~names ~extensible uctx in - let nas = UnivNames.compute_instance_binders (UContext.instance uctx) binders in + let nas = compute_instance_binders (UContext.instance uctx) binders in Entries.Polymorphic_entry (nas, uctx) else let () = check_universe_context_set ~names ~extensible uctx in |