diff options
| author | coqbot-app[bot] | 2020-11-26 11:06:00 +0000 |
|---|---|---|
| committer | GitHub | 2020-11-26 11:06:00 +0000 |
| commit | 0fc82e9651ee1dbc429c9b328b90ad8ad1a3cb14 (patch) | |
| tree | c99091031ad585bf3249ae089e12f44d4e5d83ce /library | |
| parent | 5c7f71a270b265d1ae3f86cb2a29d28f2310edc5 (diff) | |
| parent | 4011a9137fdebe16aa40cb03ba5ce32c09687c69 (diff) | |
Merge PR #13415: Separate interning and pretyping of universes
Reviewed-by: mattam82
Diffstat (limited to 'library')
| -rw-r--r-- | library/libnames.ml | 2 | ||||
| -rw-r--r-- | library/libnames.mli | 1 | ||||
| -rw-r--r-- | library/nametab.ml | 4 | ||||
| -rw-r--r-- | library/nametab.mli | 2 |
4 files changed, 6 insertions, 3 deletions
diff --git a/library/libnames.ml b/library/libnames.ml index 88b2e41855..ba1ef1e2f9 100644 --- a/library/libnames.ml +++ b/library/libnames.ml @@ -145,6 +145,8 @@ let qualid_of_dirpath ?loc dir = let (l,a) = split_dirpath dir in make_qualid ?loc l a +let qualid_of_lident lid = qualid_of_ident ?loc:lid.CAst.loc lid.CAst.v + let qualid_is_ident qid = DirPath.is_empty qid.CAst.v.dirpath diff --git a/library/libnames.mli b/library/libnames.mli index a384510879..65aca0c87d 100644 --- a/library/libnames.mli +++ b/library/libnames.mli @@ -77,6 +77,7 @@ val qualid_of_string : ?loc:Loc.t -> string -> qualid val qualid_of_path : ?loc:Loc.t -> full_path -> qualid val qualid_of_dirpath : ?loc:Loc.t -> DirPath.t -> qualid val qualid_of_ident : ?loc:Loc.t -> Id.t -> qualid +val qualid_of_lident : lident -> qualid val qualid_is_ident : qualid -> bool val qualid_path : qualid -> DirPath.t diff --git a/library/nametab.ml b/library/nametab.ml index a51c281f2b..d5cc4f8ac5 100644 --- a/library/nametab.ml +++ b/library/nametab.ml @@ -562,9 +562,9 @@ let shortest_qualid_of_modtype ?loc kn = let sp = MPmap.find kn !the_modtyperevtab in MPTab.shortest_qualid ?loc Id.Set.empty sp !the_modtypetab -let shortest_qualid_of_universe ?loc kn = +let shortest_qualid_of_universe ?loc ctx kn = let sp = UnivIdMap.find kn !the_univrevtab in - UnivTab.shortest_qualid ?loc Id.Set.empty sp !the_univtab + UnivTab.shortest_qualid ?loc ctx sp !the_univtab let pr_global_env env ref = try pr_qualid (shortest_qualid_of_global env ref) diff --git a/library/nametab.mli b/library/nametab.mli index 8a8b59733c..fa27dcab9a 100644 --- a/library/nametab.mli +++ b/library/nametab.mli @@ -206,7 +206,7 @@ val shortest_qualid_of_global : ?loc:Loc.t -> Id.Set.t -> GlobRef.t -> qualid val shortest_qualid_of_syndef : ?loc:Loc.t -> Id.Set.t -> syndef_name -> qualid val shortest_qualid_of_modtype : ?loc:Loc.t -> ModPath.t -> qualid val shortest_qualid_of_module : ?loc:Loc.t -> ModPath.t -> qualid -val shortest_qualid_of_universe : ?loc:Loc.t -> Univ.Level.UGlobal.t -> qualid +val shortest_qualid_of_universe : ?loc:Loc.t -> Id.Set.t -> Univ.Level.UGlobal.t -> qualid (** {5 Generic name handling} *) |