diff options
Diffstat (limited to 'engine/univNames.ml')
| -rw-r--r-- | engine/univNames.ml | 38 |
1 files changed, 1 insertions, 37 deletions
diff --git a/engine/univNames.ml b/engine/univNames.ml index 6d9095680c..2e15558db2 100644 --- a/engine/univNames.ml +++ b/engine/univNames.ml @@ -8,7 +8,6 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) -open Util open Names open Univ @@ -30,43 +29,8 @@ let pr_with_global_universes l = (** Local universe names of polymorphic references *) -type universe_binders = Univ.Level.t Names.Id.Map.t +type universe_binders = Level.t Names.Id.Map.t let empty_binders = Id.Map.empty -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) - in - Array.map map (Instance.to_array inst) - type univ_name_list = Names.lname list - -let universe_binders_with_opt_names orig names = - let orig = AUContext.names orig in - let orig = Array.to_list orig in - let udecl = match names with - | None -> orig - | Some udecl -> - try - List.map2 (fun orig {CAst.v = na} -> - match na with - | Anonymous -> orig - | Name id -> Name id) orig udecl - with Invalid_argument _ -> - let len = List.length orig in - CErrors.user_err ~hdr:"universe_binders_with_opt_names" - Pp.(str "Universe instance should have length " ++ int len) - in - let fold i acc na = match na with - | Name id -> Names.Id.Map.add id (Level.var i) acc - | Anonymous -> acc - in - List.fold_left_i fold 0 empty_binders udecl |