diff options
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 |