aboutsummaryrefslogtreecommitdiff
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 1bd03491a7..c7b37aba5c 100644
--- a/pretyping/arguments_renaming.ml
+++ b/pretyping/arguments_renaming.ml
@@ -43,7 +43,7 @@ let section_segment_of_reference = function
| ConstRef con -> Lib.section_segment_of_constant con
| IndRef (kn,_) | ConstructRef ((kn,_),_) ->
Lib.section_segment_of_mutual_inductive kn
- | _ -> [], Univ.LMap.empty, Univ.UContext.empty
+ | _ -> [], Univ.LMap.empty, Univ.AUContext.empty
let discharge_rename_args = function
| _, (ReqGlobal (c, names), _ as req) ->