diff options
Diffstat (limited to 'vernac/declareUniv.ml')
| -rw-r--r-- | vernac/declareUniv.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/vernac/declareUniv.ml b/vernac/declareUniv.ml index 20fa43c8e7..89f3503f4d 100644 --- a/vernac/declareUniv.ml +++ b/vernac/declareUniv.ml @@ -94,7 +94,7 @@ let do_universe ~poly l = in let src = if poly then BoundUniv else UnqualifiedUniv in let () = Lib.add_anonymous_leaf (input_univ_names (src, l)) in - Declare.declare_universe_context ~poly ctx + DeclareUctx.declare_universe_context ~poly ctx let do_constraint ~poly l = let open Univ in @@ -107,4 +107,4 @@ let do_constraint ~poly l = Constraint.empty l in let uctx = ContextSet.add_constraints constraints ContextSet.empty in - Declare.declare_universe_context ~poly uctx + DeclareUctx.declare_universe_context ~poly uctx |