diff options
| author | Pierre-Marie Pédrot | 2019-10-30 14:16:13 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2019-10-30 14:16:13 +0100 |
| commit | 7634426a7a6de08ff0ea172a0770b9a159b25934 (patch) | |
| tree | f65d556ad609d160b47379671262c64f10f893bc /vernac | |
| parent | a7371d946d44113a38d9cf217df36c23ce5e48ee (diff) | |
| parent | b27f54b04f50d3fad0eedd9c46366fd2bb612987 (diff) | |
Merge PR #10949: [declare] Provide helper for private constant inlining.
Reviewed-by: SkySkimmer
Reviewed-by: ppedrot
Diffstat (limited to 'vernac')
| -rw-r--r-- | vernac/declareObl.ml | 4 | ||||
| -rw-r--r-- | vernac/obligations.ml | 8 |
2 files changed, 4 insertions, 8 deletions
diff --git a/vernac/declareObl.ml b/vernac/declareObl.ml index 2c56f707f1..b56b9c8ce2 100644 --- a/vernac/declareObl.ml +++ b/vernac/declareObl.ml @@ -490,10 +490,8 @@ let obligation_terminator entries uctx { name; num; auto } = | [entry] -> let env = Global.env () in let ty = entry.Declare.proof_entry_type in - let body, eff = Future.force entry.Declare.proof_entry_body in - let (body, cstr) = Safe_typing.inline_private_constants env (body, eff.Evd.seff_private) in + let body, uctx = Declare.inline_private_constants ~univs:uctx env entry in let sigma = Evd.from_ctx uctx in - let sigma = Evd.merge_context_set ~sideff:true Evd.univ_rigid sigma cstr in Inductiveops.control_only_guard (Global.env ()) sigma (EConstr.of_constr body); (* Declare the obligation ourselves and drop the hook *) let prg = CEphemeron.get (ProgMap.find name !from_prg) in diff --git a/vernac/obligations.ml b/vernac/obligations.ml index c8cede1f84..4ea34e2b60 100644 --- a/vernac/obligations.ml +++ b/vernac/obligations.ml @@ -423,11 +423,9 @@ let solve_by_tac ?loc name evi t poly ctx = Pfedit.build_constant_by_tactic ~name ~poly ctx evi.evar_hyps evi.evar_concl t in let env = Global.env () in - let (body, eff) = Future.force entry.Declare.proof_entry_body in - let body = Safe_typing.inline_private_constants env (body, eff.Evd.seff_private) in - let ctx' = Evd.merge_context_set ~sideff:true Evd.univ_rigid (Evd.from_ctx ctx') (snd body) in - Inductiveops.control_only_guard env ctx' (EConstr.of_constr (fst body)); - Some (fst body, entry.Declare.proof_entry_type, Evd.evar_universe_context ctx') + let body, ctx' = Declare.inline_private_constants ~univs:ctx' env entry in + Inductiveops.control_only_guard env (Evd.from_ctx ctx') (EConstr.of_constr body); + Some (body, entry.Declare.proof_entry_type, ctx') with | Refiner.FailError (_, s) as exn -> let _ = CErrors.push exn in |