diff options
Diffstat (limited to 'vernac/comAssumption.ml')
| -rw-r--r-- | vernac/comAssumption.ml | 11 |
1 files changed, 5 insertions, 6 deletions
diff --git a/vernac/comAssumption.ml b/vernac/comAssumption.ml index 6a590758..750ed35c 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 @@ -137,7 +136,7 @@ let do_assumptions kind nl l = let open Context.Named.Declaration in let env = Global.env () in let udecl, l = process_assumptions_udecls kind l in - let sigma, udecl = Univdecls.interp_univ_decl_opt env udecl in + let sigma, udecl = interp_univ_decl_opt env udecl in let l = if pi2 kind (* poly *) then (* Separate declarations so that A B : Type puts A and B in different levels. *) @@ -158,13 +157,13 @@ let do_assumptions kind nl l = ((sigma,env,ienv),((is_coe,idl),t,imps))) (sigma,env,empty_internalization_env) l in - let sigma = solve_remaining_evars all_and_fail_flags env sigma Evd.empty in + let sigma = solve_remaining_evars all_and_fail_flags env sigma (Evd.from_env env) in (* The universe constraints come from the whole telescope. *) let sigma = Evd.minimize_universes sigma in let nf_evar c = EConstr.to_constr sigma c in let uvars, l = List.fold_left_map (fun uvars (coe,t,imps) -> let t = nf_evar t in - let uvars = Univ.LSet.union uvars (Univops.universes_of_constr env t) in + let uvars = Univ.LSet.union uvars (Univops.universes_of_constr t) in uvars, (coe,t,imps)) Univ.LSet.empty l in @@ -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) |