diff options
| author | Pierre-Marie Pédrot | 2018-09-13 16:42:29 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2018-10-08 15:38:35 +0200 |
| commit | a7e3a426886c712528a7561fb351e0234e4de2bc (patch) | |
| tree | d1ad0d3db8b4c3687dfefffed04636348967b861 | |
| parent | 9a1cbeb18e10e7eb40363e648e15f4f9aae1f9b8 (diff) | |
Remove dead code in universe handling in the abstract tactical.
Since 213b323 the kernel was expecting to receive an empty set of internal
universe constraints in polymorphic definitions. We lift this invariant to
the code that actually generates side effects.
| -rw-r--r-- | tactics/tactics.ml | 24 |
1 files changed, 10 insertions, 14 deletions
diff --git a/tactics/tactics.ml b/tactics/tactics.ml index f3f81ff616..3769dca6e0 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -5017,21 +5017,17 @@ let cache_term_by_tactic_then ~opaque ?(goal_type=None) id gk tac tacK = Declare.declare_constant ~internal:Declare.InternalTacticRequest ~local:true id decl in let cst = Impargs.with_implicit_protection cst () in - let lem = - match const.Entries.const_entry_universes with - | Entries.Polymorphic_const_entry uctx -> - let uctx = Univ.ContextSet.of_context uctx in - (** Hack: the kernel may generate definitions whose universe variables are - not the same as requested in the entry because of constraints delayed - in the body, even in polymorphic mode. We mimick what it does for now - in hope it is fixed at some point. *) - let (_, body_uctx), _ = Future.force const.Entries.const_entry_body in - let uctx = Univ.ContextSet.to_context (Univ.ContextSet.union uctx body_uctx) in - let u = Univ.UContext.instance uctx in - mkConstU (cst, EInstance.make u) - | Entries.Monomorphic_const_entry _ -> - mkConst cst + let inst = match const.Entries.const_entry_universes with + | Entries.Monomorphic_const_entry _ -> EInstance.empty + | Entries.Polymorphic_const_entry ctx -> + (** We mimick what the kernel does, that is ensuring that no additional + constraints appear in the body of polymorphic constants. Ideally this + should be enforced statically. *) + let (_, body_uctx), _ = Future.force const.Entries.const_entry_body in + let () = assert (Univ.ContextSet.is_empty body_uctx) in + EInstance.make (Univ.UContext.instance ctx) in + let lem = mkConstU (cst, inst) in let evd = Evd.set_universe_context evd ectx in let open Safe_typing in let eff = private_con_of_con (Global.safe_env ()) cst in |