diff options
| author | Gaëtan Gilbert | 2019-07-02 12:35:49 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2019-07-03 17:01:29 +0200 |
| commit | d324c858be652659a5062332f00e7d20393a48be (patch) | |
| tree | 8e36d767d1a11e47e9c825c3a8e96fd0f7fddf87 /tactics | |
| parent | 5a6de0ece2436a0fe49750ba0ec26da90f0417e3 (diff) | |
Safe_typing.push_named_assum: don't take universes
The caller should push them first
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/declare.ml | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/tactics/declare.ml b/tactics/declare.ml index dbf570eaad..ed745b1269 100644 --- a/tactics/declare.ml +++ b/tactics/declare.ml @@ -311,9 +311,10 @@ let cache_variable (_,o) = let impl,opaque,poly,univs = match d with (* Fails if not well-typed *) | SectionLocalAssum {typ;univs;poly;impl} -> - let () = Global.push_named_assum ((id,typ,poly),univs) in + let () = Global.push_context_set poly univs in + let () = Global.push_named_assum (id,typ) in let impl = if impl then Decl_kinds.Implicit else Decl_kinds.Explicit in - impl, true, poly, univs + impl, true, poly, univs | SectionLocalDef (de) -> (* The body should already have been forced upstream because it is a section-local definition, but it's not enforced by typing *) |