diff options
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)) |