diff options
Diffstat (limited to 'vernac/comAssumption.ml')
| -rw-r--r-- | vernac/comAssumption.ml | 5 |
1 files changed, 2 insertions, 3 deletions
diff --git a/vernac/comAssumption.ml b/vernac/comAssumption.ml index 6a590758f..722f21171 100644 --- a/vernac/comAssumption.ml +++ b/vernac/comAssumption.ml @@ -20,7 +20,6 @@ open Constrintern open Impargs open Decl_kinds open Pretyping -open Vernacexpr open Entries (* 2| Variable/Hypothesis/Parameter/Axiom declarations *) @@ -66,7 +65,7 @@ match local with | Global | Local | Discharge -> let do_instance = should_axiom_into_instance local in let local = DeclareDef.get_locality ident ~kind:"axiom" local in - let inl = match nl with + let inl = let open Declaremods in match nl with | NoInline -> None | DefaultInline -> Some (Flags.get_inline_level()) | InlineAt i -> Some i @@ -175,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) |