diff options
| author | ppedrot | 2013-08-05 21:01:52 +0000 |
|---|---|---|
| committer | ppedrot | 2013-08-05 21:01:52 +0000 |
| commit | acd450f5c2eef92a1079b674a5cc4575f627ae45 (patch) | |
| tree | cbf71e10751868a5190dd2ab88f4b3120d8c71a3 /lib | |
| parent | 7ab24497b8d66a96a706db3be0400a962cbc092f (diff) | |
Tentative fix for bug #2961. When we have to print two terms that
should be different, we compute the externalized form for both in
the current state. If ever they coincide, we do it again with the
implicit arguments flag set.
In other words, if those two terms appear the same, we automatically
print them with the implicit arguments flag on.
This is a bit raw, and we may try other externalization flags, but
I assume it to be (almost) sufficient for now.
TODO: check every place where we could need such a feature, and try
other flags.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16664 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'lib')
0 files changed, 0 insertions, 0 deletions