diff options
| author | Chantal Keller <Chantal.Keller@lri.fr> | 2016-10-07 14:07:25 +0200 |
|---|---|---|
| committer | Chantal Keller <Chantal.Keller@lri.fr> | 2016-10-07 14:07:25 +0200 |
| commit | 3fb5bc25ded5ba737ec3c62d2cc49e240fc9cc3e (patch) | |
| tree | 2a08085fd8a9a0b9651d96b647d777e928cb6274 /src/versions | |
| parent | e0dcd7c140cfec89300fa9f0a8a0f9b8d12633e0 (diff) | |
| download | smtcoq-3fb5bc25ded5ba737ec3c62d2cc49e240fc9cc3e.tar.gz smtcoq-3fb5bc25ded5ba737ec3c62d2cc49e240fc9cc3e.zip | |
(Hopefully) repared the universes problems
Diffstat (limited to 'src/versions')
| -rw-r--r-- | src/versions/standard/structures.ml | 5 |
1 files changed, 4 insertions, 1 deletions
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 |