diff options
| author | Pierre-Marie Pédrot | 2016-11-25 11:36:09 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2017-02-14 17:30:39 +0100 |
| commit | 778e863b77bcafc8ed339dd02226e85e5fee2532 (patch) | |
| tree | c836854265a6c1ac401b524710a0b7947bea3d37 /ide | |
| parent | 05afd04095e35d77ca135bd2c1cb8d303ea2d6a8 (diff) | |
Removing compatibility layers related to printing.
Diffstat (limited to 'ide')
| -rw-r--r-- | ide/ide_slave.ml | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/ide/ide_slave.ml b/ide/ide_slave.ml index c11c785877..fcba013535 100644 --- a/ide/ide_slave.ml +++ b/ide/ide_slave.ml @@ -192,6 +192,7 @@ let process_goal sigma g = let id = Goal.uid g in let ccl = let norm_constr = Reductionops.nf_evar sigma (EConstr.Unsafe.to_constr (Goal.V82.concl sigma g)) in + let norm_constr = EConstr.of_constr norm_constr in Richpp.richpp_of_pp (pr_goal_concl_style_env env sigma norm_constr) in let process_hyp d (env,l) = |