Evar-normalizing functions now act on EConstrs.

1 files changed, 2 insertions, 3 deletions

diff --git a/ide/ide_slave.ml b/ide/ide_slave.ml
index fcba013535..8fc5547ece 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