From 3fb5bc25ded5ba737ec3c62d2cc49e240fc9cc3e Mon Sep 17 00:00:00 2001 From: Chantal Keller Date: Fri, 7 Oct 2016 14:07:25 +0200 Subject: (Hopefully) repared the universes problems --- src/versions/standard/structures.ml | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) (limited to 'src/versions') diff --git a/src/versions/standard/structures.ml b/src/versions/standard/structures.ml index 168c9b2..19104fe 100644 --- a/src/versions/standard/structures.ml +++ b/src/versions/standard/structures.ml @@ -120,7 +120,10 @@ let declare_new_type t = Term.mkVar t let declare_new_variable v constr_t = - let _ = Command.declare_assumption false (Decl_kinds.Discharge, false, Decl_kinds.Definitional) (constr_t, Univ.ContextSet.empty) [] [] false Vernacexpr.NoInline (dummy_loc, v) in + let env = Global.env () in + let evd = Evd.from_env env in + let evd, _ = Typing.type_of env evd constr_t in + let _ = Command.declare_assumption false (Decl_kinds.Discharge, false, Decl_kinds.Definitional) (constr_t, Evd.universe_context_set evd) [] [] false Vernacexpr.NoInline (dummy_loc, v) in Term.mkVar v let extern_constr = Constrextern.extern_constr true Environ.empty_env Evd.empty -- cgit