diff options
| author |  Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2017-09-21 00:53:10 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2017-11-25 14:18:35 +0100 |
| commit | 765392492df2f5e065b2b5e706b6620846337cc0 (patch) | |
| tree | ccf14d9040e76acca2a902cdefa57fefc53bc64a /vernac/lemmas.ml | |
| parent | 280c922fc55b57c430cad721c83650a796a375fd (diff) | |
Universe binders survive sections, modules and compilation.
Diffstat (limited to 'vernac/lemmas.ml')
| -rw-r--r-- | vernac/lemmas.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml index a787ec6fa..42631a15b 100644 --- a/vernac/lemmas.ml +++ b/vernac/lemmas.ml @@ -204,7 +204,7 @@ let save ?export_seff id const cstrs pl do_guard (locality,poly,kind) hook = (locality, ConstRef kn) in definition_message id; - Option.iter (Universes.register_universe_binders r) pl; + Universes.register_universe_binders r (Option.default Universes.empty_binders pl); call_hook (fun exn -> exn) hook l r with e when CErrors.noncritical e -> let e = CErrors.push e in @@ -312,7 +312,7 @@ let admit (id,k,e) pl hook () = | Local, _, _ | Discharge, _, _ -> warn_let_as_axiom id in let () = assumption_message id in - Option.iter (Universes.register_universe_binders (ConstRef kn)) pl; + Universes.register_universe_binders (ConstRef kn) (Option.default Universes.empty_binders pl); call_hook (fun exn -> exn) hook Global (ConstRef kn) (* Starting a goal *) |