diff options
| author |  Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2017-09-18 17:22:24 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2017-11-24 19:23:41 +0100 |
| commit | 34d85e1e899f8a045659ccc53bfd6a1f5104130b (patch) | |
| tree | ed176f6f7d0d47802d5c4e1879cd2eb35232df46 /vernac/declareDef.ml | |
| parent | 58c0784745f8b2ba7523f246c4611d780c9f3f70 (diff) | |
Use Entries.constant_universes_entry more.
This reduces conversions between ContextSet/UContext and encodes
whether we are polymorphic by which constructor we use rather than
using some boolean.
Diffstat (limited to 'vernac/declareDef.ml')
| -rw-r--r-- | vernac/declareDef.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/vernac/declareDef.ml b/vernac/declareDef.ml index c18744052..980db4109 100644 --- a/vernac/declareDef.ml +++ b/vernac/declareDef.ml @@ -57,7 +57,7 @@ let declare_definition ident (local, p, k) ce pl imps hook = declare_global_definition ident ce local k pl imps in Lemmas.call_hook fix_exn hook local r -let declare_fix ?(opaque = false) (_,poly,_ as kind) pl ctx f ((def,_),eff) t imps = - let ce = definition_entry ~opaque ~types:t ~poly ~univs:ctx ~eff def in +let declare_fix ?(opaque = false) (_,poly,_ as kind) pl univs f ((def,_),eff) t imps = + let ce = definition_entry ~opaque ~types:t ~univs ~eff def in declare_definition f kind ce pl imps (Lemmas.mk_hook (fun _ r -> r)) |