diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-07-13 00:50:02 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-07-14 13:00:41 +0200 |
| commit | 6806059f7c043b45e6c42f382f069f8c49ed1c1f (patch) | |
| tree | 32e020671754f9606288623e6df543cecb90ac10 /tactics/tactics.ml | |
| parent | 0411c7e08b58edc4785c2be396fad0a037056a11 (diff) | |
Getting rid of abstraction breaking code in tclABSTRACT.
This is probably the hardest case of them all, because tclABSTRACT fundamentally
relies on the names of universes from the constant instance being the same as
the one in the current goal. Adding to that the fact that the kernel is doing
strange things when provided with a polymorphic definition with body universe
constraints, it turns out to be a hellish nightmare to handle properly.
At some point we need to clarifiy this in the kernel as well, although we
leave it for some other patch.
Diffstat (limited to 'tactics/tactics.ml')
| -rw-r--r-- | tactics/tactics.ml | 18 |
1 files changed, 13 insertions, 5 deletions
diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 177c44bcb..c979b8b04 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -5003,11 +5003,19 @@ 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 evd, lem = Evd.fresh_global (Global.env ()) evd (ConstRef cst) in *) - let lem, ctx = Global.constr_of_global_in_context (Global.env ()) (ConstRef cst) in - let inst = Univ.AUContext.instance ctx in - let lem = CVars.subst_instance_constr inst lem in - let lem = EConstr.of_constr lem in + let lem = + if const.Entries.const_entry_polymorphic then + let uctx = Univ.ContextSet.of_context const.Entries.const_entry_universes 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) + else mkConst cst + 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 |