summaryrefslogtreecommitdiff
path: root/pretyping/arguments_renaming.ml
diff options
context:
space:
mode:
Diffstat (limited to 'pretyping/arguments_renaming.ml')
-rw-r--r--pretyping/arguments_renaming.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/pretyping/arguments_renaming.ml b/pretyping/arguments_renaming.ml
index 84295959..9d4badc6 100644
--- a/pretyping/arguments_renaming.ml
+++ b/pretyping/arguments_renaming.ml
@@ -26,7 +26,7 @@ let name_table =
type req =
| ReqLocal
- | ReqGlobal of global_reference * Name.t list
+ | ReqGlobal of GlobRef.t * Name.t list
let load_rename_args _ (_, (_, (r, names))) =
name_table := Refmap.add r names !name_table