diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2014-10-22 17:47:43 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2014-10-22 17:50:06 +0200 |
| commit | 3c199388700c523932761c56a423577ef7aee7f2 (patch) | |
| tree | c4ac68cce808f595f163510ef17eeb5ce13afb8e /ide/ide_slave.ml | |
| parent | 116ec0eb91ce05d21433c1127636f2abf4ec55c4 (diff) | |
Pushing Pierre's factorization of names in goal context printing from
coqide to coqtop.
(Joint work with Pierre)
Diffstat (limited to 'ide/ide_slave.ml')
| -rw-r--r-- | ide/ide_slave.ml | 13 |
1 files changed, 2 insertions, 11 deletions
diff --git a/ide/ide_slave.ml b/ide/ide_slave.ml index 1df9d0fc3..a91be2aa4 100644 --- a/ide/ide_slave.ml +++ b/ide/ide_slave.ml @@ -168,16 +168,6 @@ let concl_next_tac sigma concl = "right" ]) -let compact_named_context c = - let compact l (i1,c1,t1) = - match l with - | [] -> [[i1],c1,t1] - | (l2,c2,t2)::q -> - if Option.equal Constr.equal c1 c2 && Constr.equal t1 t2 - then (i1::l2,c2,t2)::q - else ([i1],c1,t1)::l - in Context.fold_named_context_reverse compact ~init:[] c - let process_goal sigma g = let env = Goal.V82.env sigma g in let min_env = Environ.reset_context env in @@ -189,7 +179,8 @@ let process_goal sigma g = let d = Context.map_named_list_declaration (Reductionops.nf_evar sigma) d in (string_of_ppcmds (pr_var_list_decl min_env sigma d)) in let hyps = - List.map process_hyp (compact_named_context (Environ.named_context env)) in + List.map process_hyp + (Termops.compact_named_context (Environ.named_context env)) in { Interface.goal_hyp = hyps; Interface.goal_ccl = ccl; Interface.goal_id = id; } let goals () = |