diff options
| author | Vincent Laporte | 2018-09-07 17:17:19 +0200 |
|---|---|---|
| committer | Vincent Laporte | 2018-09-12 16:05:18 +0000 |
| commit | 8fafc201699e3d6c80e39bbadf2e6a5ba6425036 (patch) | |
| tree | 7580d72ad191ec54758deba3a662967d0fe9e5e3 /interp/impargs.ml | |
| parent | 26936e66c7c16f72fd1a7978505c95af9899ddc0 (diff) | |
Move maps & sets indexed by GlobRef.t into the kernel
Diffstat (limited to 'interp/impargs.ml')
| -rw-r--r-- | interp/impargs.ml | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/interp/impargs.ml b/interp/impargs.ml index e542b818f6..3603367cf1 100644 --- a/interp/impargs.ml +++ b/interp/impargs.ml @@ -508,11 +508,11 @@ type implicit_discharge_request = | ImplInteractive of GlobRef.t * implicits_flags * implicit_interactive_request -let implicits_table = Summary.ref Refmap.empty ~name:"implicits" +let implicits_table = Summary.ref GlobRef.Map.empty ~name:"implicits" let implicits_of_global ref = try - let l = Refmap.find ref !implicits_table in + let l = GlobRef.Map.find ref !implicits_table in try let rename_l = Arguments_renaming.arguments_names ref in let rec rename implicits names = match implicits, names with @@ -527,7 +527,7 @@ let implicits_of_global ref = with Not_found -> [DefaultImpArgs,[]] let cache_implicits_decl (ref,imps) = - implicits_table := Refmap.add ref imps !implicits_table + implicits_table := GlobRef.Map.add ref imps !implicits_table let load_implicits _ (_,(_,l)) = List.iter cache_implicits_decl l |