aboutsummaryrefslogtreecommitdiffhomepage
path: root/vernac/comAssumption.ml
diff options
context:
space:
mode:
Diffstat (limited to 'vernac/comAssumption.ml')
-rw-r--r--vernac/comAssumption.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/vernac/comAssumption.ml b/vernac/comAssumption.ml
index 26a46a752..722f21171 100644
--- a/vernac/comAssumption.ml
+++ b/vernac/comAssumption.ml
@@ -174,7 +174,7 @@ let do_assumptions kind nl l =
let t = replace_vars subst t in
let refs, status' = declare_assumptions idl is_coe kind (t,uctx) ubinders imps nl in
let subst' = List.map2
- (fun {CAst.v=id} (c,u) -> (id, Universes.constr_of_global_univ (c,u)))
+ (fun {CAst.v=id} (c,u) -> (id, UnivGen.constr_of_global_univ (c,u)))
idl refs
in
subst'@subst, status' && status, next_uctx uctx)