diff options
| author | Emilio Jesus Gallego Arias | 2020-06-30 15:57:33 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2020-06-30 15:57:33 +0200 |
| commit | 9c9330f2e3a5ff205973881003c5734034b7d0d5 (patch) | |
| tree | ba410bd04083fe3f8bf6a0f70fb4a1fa66663115 /printing/printer.ml | |
| parent | bffe3e8dcbb6019b30d32081f0b56eba30bf8be7 (diff) | |
| parent | 6bb0c6df0dd331b8acb78a720eaf076aea5fce47 (diff) | |
Merge PR #12599: Remove the Refiner module
Reviewed-by: ejgallego
Diffstat (limited to 'printing/printer.ml')
| -rw-r--r-- | printing/printer.ml | 3 |
1 files changed, 1 insertions, 2 deletions
diff --git a/printing/printer.ml b/printing/printer.ml index b0a4c8b738..96213b3b8b 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 @@ -453,7 +452,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 = |