From e2a81df304c198cc2bdd5d1ffa703ed7eaca9d12 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Sun, 23 Jul 2017 04:08:30 +0200 Subject: Remove a few useless evar-normalizations in printing code. --- ide/ide_slave.ml | 6 ++---- 1 file changed, 2 insertions(+), 4 deletions(-) (limited to 'ide') diff --git a/ide/ide_slave.ml b/ide/ide_slave.ml index cb2b365a4..67391f556 100644 --- a/ide/ide_slave.ml +++ b/ide/ide_slave.ml @@ -177,11 +177,9 @@ 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 (Goal.V82.concl sigma g) in - pr_goal_concl_style_env env sigma norm_constr + pr_goal_concl_style_env env sigma (Goal.V82.concl sigma g) in let process_hyp d (env,l) = - 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, (pr_compacted_decl env sigma d) :: l) in @@ -210,7 +208,7 @@ let evars () = Stm.finish (); let pfts = Proof_global.give_me_the_proof () in let { Evd.it = all_goals ; sigma = sigma } = Proof.V82.subgoals pfts in - let exl = Evar.Map.bindings (Evarutil.non_instantiated sigma) in + let exl = Evar.Map.bindings (Evd.undefined_map sigma) in let map_evar ev = { Interface.evar_info = string_of_ppcmds (pr_evar sigma ev); } in let el = List.map map_evar exl in Some el -- cgit v1.2.3