diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-10-04 12:03:52 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-10-04 12:03:52 +0000 |
| commit | e892cdd483eca0c880f338f1e4fd7deecdfc5501 (patch) | |
| tree | 077bcdc3e3a7b7b3f2aa572ba1130ade924de3a0 /tactics | |
| parent | ee3c7ddaf0ab726594b278d30430123cd60e63fa (diff) | |
Fixing bugs in previous commits about implicit arguments:
- fixing r13483 (supposed dead code in impargs was actually half-living:
implicit arguments mode should merge with the {...} manually given
implicit arguments but not with the "Implicit Arguments [...]" arguments),
- fixing code of drop_first_implicits in r13484.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13490 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'tactics')
0 files changed, 0 insertions, 0 deletions