diff options
Diffstat (limited to 'printing/proof_diffs.ml')
| -rw-r--r-- | printing/proof_diffs.ml | 9 |
1 files changed, 6 insertions, 3 deletions
diff --git a/printing/proof_diffs.ml b/printing/proof_diffs.ml index d620e14a94..ab4501fe75 100644 --- a/printing/proof_diffs.ml +++ b/printing/proof_diffs.ml @@ -547,13 +547,16 @@ let match_goals ot nt = | None -> ()); !nevar_to_oevar +let get_proof_context (p : Proof.t) = + let Proof.{goals; sigma} = Proof.data p in + sigma, Refiner.pf_env { Evd.it = List.(hd goals); sigma } -let to_constr p = +let to_constr pf = let open CAst in - let pprf = Proof.partial_proof p in + let pprf = Proof.partial_proof pf in (* pprf generally has only one element, but it may have more in the derive plugin *) let t = List.hd pprf in - let sigma, env = Pfedit.get_current_context ~p () in + let sigma, env = get_proof_context pf in let x = Constrextern.extern_constr false env sigma t in (* todo: right options?? *) x.v |