diff options
Diffstat (limited to 'engine/uState.ml')
| -rw-r--r-- | engine/uState.ml | 7 |
1 files changed, 1 insertions, 6 deletions
diff --git a/engine/uState.ml b/engine/uState.ml index ff60a5f9d4..d4cb59da26 100644 --- a/engine/uState.ml +++ b/engine/uState.ml @@ -114,16 +114,11 @@ let constraints ctx = snd ctx.local let context ctx = ContextSet.to_context ctx.local -let name_universe lvl = - (* Best-effort naming from the string representation of the level. This is - completely hackish and should be solved in upper layers instead. *) - Id.of_string_soft (Level.to_string lvl) - 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 -> Name (name_universe lvl) + with Not_found -> Anonymous in Array.map map (Instance.to_array inst) |