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/obligations.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/obligations.ml')
| -rw-r--r-- | vernac/obligations.ml | 17 |
1 files changed, 5 insertions, 12 deletions
diff --git a/vernac/obligations.ml b/vernac/obligations.ml index a9110c76c..97cdd7977 100644 --- a/vernac/obligations.ml +++ b/vernac/obligations.ml @@ -475,12 +475,8 @@ let declare_definition prg = (Evd.evar_universe_context_subst prg.prg_ctx) in let opaque = prg.prg_opaque in let fix_exn = Hook.get get_fix_exn () in - let () = ignore(UState.check_univ_decl prg.prg_ctx prg.prg_univdecl) in - let ce = - definition_entry ~fix_exn - ~opaque ~types:(nf typ) ~poly:(pi2 prg.prg_kind) - ~univs:(UState.context prg.prg_ctx) (nf body) - in + let univs = UState.check_univ_decl ~poly:(pi2 prg.prg_kind) prg.prg_ctx prg.prg_univdecl in + let ce = definition_entry ~fix_exn ~opaque ~types:(nf typ) ~univs (nf body) in let () = progmap_remove prg in let ubinders = UState.universe_binders prg.prg_ctx in DeclareDef.declare_definition prg.prg_name @@ -549,9 +545,9 @@ let declare_mutual_definition l = mk_proof (mkCoFix (i,fixdecls))) 0 l in (* Declare the recursive definitions *) - let ctx = UState.context first.prg_ctx in + let univs = UState.const_univ_entry ~poly first.prg_ctx in let fix_exn = Hook.get get_fix_exn () in - let kns = List.map4 (DeclareDef.declare_fix ~opaque (local, poly, kind) Universes.empty_binders ctx) + let kns = List.map4 (DeclareDef.declare_fix ~opaque (local, poly, kind) Universes.empty_binders univs) fixnames fixdecls fixtypes fiximps in (* Declare notations *) List.iter (Metasyntax.add_notation_interpretation (Global.env())) first.prg_notations; @@ -856,10 +852,7 @@ let obligation_terminator name num guard hook auto pf = | (_, status), Vernacexpr.Transparent -> status in let obl = { obl with obl_status = false, status } in - let uctx = if pi2 prg.prg_kind - then Polymorphic_const_entry (UState.context ctx) - else Monomorphic_const_entry (UState.context_set ctx) - in + let uctx = UState.const_univ_entry ~poly:(pi2 prg.prg_kind) ctx in let (_, obl) = declare_obligation prg obl body ty uctx in let obls = Array.copy obls in let _ = obls.(num) <- obl in |