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 /kernel/nativecode.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 'kernel/nativecode.ml')
0 files changed, 0 insertions, 0 deletions