diff options
Diffstat (limited to 'tuto1/src/simple_declare.ml')
| -rw-r--r-- | tuto1/src/simple_declare.ml | 7 |
1 files changed, 3 insertions, 4 deletions
diff --git a/tuto1/src/simple_declare.ml b/tuto1/src/simple_declare.ml index 5fd0b2e84b..10fa640548 100644 --- a/tuto1/src/simple_declare.ml +++ b/tuto1/src/simple_declare.ml @@ -1,11 +1,10 @@ let edeclare ident (_, poly, _ as k) ~opaque sigma udecl body tyopt imps hook = let open EConstr in - let env = Global.env () in let sigma = Evd.minimize_universes sigma in let body = to_constr sigma body in let tyopt = Option.map (to_constr sigma) tyopt in let uvars_fold uvars c = - Univ.LSet.union uvars (Univops.universes_of_constr env c) in + Univ.LSet.union uvars (Univops.universes_of_constr c) in let uvars = List.fold_left uvars_fold Univ.LSet.empty (Option.List.cons tyopt [body]) in let sigma = Evd.restrict_universe_context sigma uvars in @@ -19,8 +18,8 @@ let packed_declare_definition ident value_with_constraints = let sigma = Evd.from_ctx ctx in let k = (Decl_kinds.Global, Flags.is_universe_polymorphism(), Decl_kinds.Definition) in - let udecl = Univdecls.default_univ_decl in + let udecl = UState.default_univ_decl in let nohook = Lemmas.mk_hook (fun _ x -> x) in ignore (edeclare ident k ~opaque:false sigma udecl body None [] nohook) -(* But this definition cannot be undone by Reset ident *)
\ No newline at end of file +(* But this definition cannot be undone by Reset ident *) |