diff options
| author | Maxime Dénès | 2018-09-13 18:07:55 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2018-09-13 18:07:55 +0200 |
| commit | 8500216ac8df90b2afc0f5fd42d714cc87c6bde6 (patch) | |
| tree | 76a1ebe10646d2432f1539fb7ee9c6b0691ea221 /engine | |
| parent | 9281bb33f2b9aa5d762f8b5b8b0159984b696efb (diff) | |
| parent | 8fafc201699e3d6c80e39bbadf2e6a5ba6425036 (diff) | |
Merge PR #8436: Move maps & sets indexed by GlobRef.t into the kernel
Diffstat (limited to 'engine')
| -rw-r--r-- | engine/namegen.ml | 6 | ||||
| -rw-r--r-- | engine/univNames.ml | 7 |
2 files changed, 6 insertions, 7 deletions
diff --git a/engine/namegen.ml b/engine/namegen.ml index 978f33b683..2a59b914db 100644 --- a/engine/namegen.ml +++ b/engine/namegen.ml @@ -258,15 +258,15 @@ let restart_subscript id = forget_subscript id let visible_ids sigma (nenv, c) = - let accu = ref (Refset_env.empty, Int.Set.empty, Id.Set.empty) in + let accu = ref (GlobRef.Set_env.empty, Int.Set.empty, Id.Set.empty) in let rec visible_ids n c = match EConstr.kind sigma c with | Const _ | Ind _ | Construct _ | Var _ as c -> let (gseen, vseen, ids) = !accu in let g = global_of_constr c in - if not (Refset_env.mem g gseen) then + if not (GlobRef.Set_env.mem g gseen) then begin try - let gseen = Refset_env.add g gseen in + let gseen = GlobRef.Set_env.add g gseen in let short = shortest_qualid_of_global Id.Set.empty g in let dir, id = repr_qualid short in let ids = if DirPath.is_empty dir then Id.Set.add id ids else ids in diff --git a/engine/univNames.ml b/engine/univNames.ml index a688401741..e861913de2 100644 --- a/engine/univNames.ml +++ b/engine/univNames.ml @@ -10,7 +10,6 @@ open Names open Univ -open Globnames open Nametab @@ -51,15 +50,15 @@ type universe_binders = Univ.Level.t Names.Id.Map.t let empty_binders = Id.Map.empty -let universe_binders_table = Summary.ref Refmap.empty ~name:"universe binders" +let universe_binders_table = Summary.ref GlobRef.Map.empty ~name:"universe binders" let universe_binders_of_global ref : universe_binders = try - let l = Refmap.find ref !universe_binders_table in l + let l = GlobRef.Map.find ref !universe_binders_table in l with Not_found -> Names.Id.Map.empty let cache_ubinder (_,(ref,l)) = - universe_binders_table := Refmap.add ref l !universe_binders_table + universe_binders_table := GlobRef.Map.add ref l !universe_binders_table let subst_ubinder (subst,(ref,l as orig)) = let ref' = fst (Globnames.subst_global subst ref) in |