diff options
| author | Maxime Dénès | 2019-03-28 13:36:52 +0100 |
|---|---|---|
| committer | Maxime Dénès | 2019-03-28 13:36:52 +0100 |
| commit | 688e20c432d2639050a62703e1c566ddfbe42b2a (patch) | |
| tree | 3b34d3bd3b73a42a8eb730a3bb6c0e6a5cb00a5f /printing/proof_diffs.ml | |
| parent | 6d0ffe795f6f29730d59c379285201fd46023935 (diff) | |
| parent | 91dfe5163fd4405977ad8fc8fe178ba5bcd73c88 (diff) | |
Merge PR #9129: [proof] Removal of imperative state ; interpretation layers only.
Ack-by: SkySkimmer
Reviewed-by: aspiwack
Ack-by: ejgallego
Ack-by: gares
Ack-by: herbelin
Reviewed-by: mattam82
Ack-by: maximedenes
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 |