diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-07-23 04:08:30 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-07-26 15:42:46 +0200 |
| commit | e2a81df304c198cc2bdd5d1ffa703ed7eaca9d12 (patch) | |
| tree | e38618f0a419d539bb1375334a56fc928a468591 /ide | |
| parent | bd1a0abf49fe67e7f02dc562d4b81d27ed6f606c (diff) | |
Remove a few useless evar-normalizations in printing code.
Diffstat (limited to 'ide')
| -rw-r--r-- | ide/ide_slave.ml | 6 |
1 files changed, 2 insertions, 4 deletions
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 |