diff options
| author | Hugo Herbelin | 2014-10-22 17:47:43 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2014-10-22 17:50:06 +0200 |
| commit | 3c199388700c523932761c56a423577ef7aee7f2 (patch) | |
| tree | c4ac68cce808f595f163510ef17eeb5ce13afb8e /pretyping | |
| parent | 116ec0eb91ce05d21433c1127636f2abf4ec55c4 (diff) | |
Pushing Pierre's factorization of names in goal context printing from
coqide to coqtop.
(Joint work with Pierre)
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/termops.ml | 10 | ||||
| -rw-r--r-- | pretyping/termops.mli | 1 |
2 files changed, 11 insertions, 0 deletions
diff --git a/pretyping/termops.ml b/pretyping/termops.ml index 5813cd416d..a1f1f52ff3 100644 --- a/pretyping/termops.ml +++ b/pretyping/termops.ml @@ -940,6 +940,16 @@ let rec mem_named_context id = function | _ :: sign -> mem_named_context id sign | [] -> false +let compact_named_context sign = + 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:[] sign + let clear_named_body id env = let aux _ = function | (id',Some c,t) when Id.equal id id' -> push_named (id,None,t) diff --git a/pretyping/termops.mli b/pretyping/termops.mli index 826104f59b..cbb9fb4ebf 100644 --- a/pretyping/termops.mli +++ b/pretyping/termops.mli @@ -215,6 +215,7 @@ val fold_named_context_both_sides : ('a -> named_declaration -> named_declaration list -> 'a) -> named_context -> init:'a -> 'a val mem_named_context : Id.t -> named_context -> bool +val compact_named_context : named_context -> named_list_context val clear_named_body : Id.t -> env -> env |