diff options
Diffstat (limited to 'ide/ide_slave.ml')
| -rw-r--r-- | ide/ide_slave.ml | 5 |
1 files changed, 2 insertions, 3 deletions
diff --git a/ide/ide_slave.ml b/ide/ide_slave.ml index fcba01353..8fc5547ec 100644 --- a/ide/ide_slave.ml +++ b/ide/ide_slave.ml @@ -191,12 +191,11 @@ let process_goal sigma g = let min_env = Environ.reset_context env in 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 + let norm_constr = Reductionops.nf_evar sigma (Goal.V82.concl sigma g) in Richpp.richpp_of_pp (pr_goal_concl_style_env env sigma norm_constr) in let process_hyp d (env,l) = - let d = CompactedDecl.map_constr (Reductionops.nf_evar sigma) d in + let d = CompactedDecl.map_constr (fun c -> EConstr.Unsafe.to_constr (Reductionops.nf_evar sigma (EConstr.of_constr c))) d in let d' = CompactedDecl.to_named_context d in (List.fold_right Environ.push_named d' env, (Richpp.richpp_of_pp (pr_compacted_decl env sigma d)) :: l) in |