diff options
| author | Pierre-Marie Pédrot | 2020-06-26 12:43:23 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-06-29 15:17:20 +0200 |
| commit | f34dcb97406611704c93970ea623d6a8587e5ba8 (patch) | |
| tree | 5a636c498c4c3fad7c15cc266dd8a386b85123e1 /printing | |
| parent | e5b355107d985d7efe2976b9eee9b6c182e25f24 (diff) | |
Moving the remaining Refiner functions to Tacmach.
Diffstat (limited to 'printing')
| -rw-r--r-- | printing/printer.ml | 3 | ||||
| -rw-r--r-- | printing/proof_diffs.ml | 4 |
2 files changed, 3 insertions, 4 deletions
diff --git a/printing/printer.ml b/printing/printer.ml index 2ad9e268c2..37b8b244a3 100644 --- a/printing/printer.ml +++ b/printing/printer.ml @@ -16,7 +16,6 @@ open Constr open Context open Environ open Evd -open Refiner open Constrextern open Ppconstr open Declarations @@ -421,7 +420,7 @@ let pr_transparent_state ts = *) let pr_goal ?(diffs=false) ?og_s g_s = let g = sig_it g_s in - let sigma = project g_s in + let sigma = Tacmach.project g_s in let env = Goal.V82.env sigma g in let concl = Goal.V82.concl sigma g in let goal = diff --git a/printing/proof_diffs.ml b/printing/proof_diffs.ml index c78cc96a83..43f70dfecc 100644 --- a/printing/proof_diffs.ml +++ b/printing/proof_diffs.ml @@ -335,7 +335,7 @@ let unwrap g_s = match g_s with | Some g_s -> let goal = Evd.sig_it g_s in - let sigma = Refiner.project g_s in + let sigma = Tacmach.project g_s in goal_info goal sigma | None -> ([], CString.Map.empty, Pp.mt ()) @@ -545,7 +545,7 @@ let match_goals ot nt = 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 } + sigma, Tacmach.pf_env { Evd.it = List.(hd goals); sigma } let to_constr pf = let open CAst in |