aboutsummaryrefslogtreecommitdiff
path: root/dev
diff options
context:
space:
mode:
authorherbelin2010-10-04 12:03:52 +0000
committerherbelin2010-10-04 12:03:52 +0000
commite892cdd483eca0c880f338f1e4fd7deecdfc5501 (patch)
tree077bcdc3e3a7b7b3f2aa572ba1130ade924de3a0 /dev
parentee3c7ddaf0ab726594b278d30430123cd60e63fa (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 'dev')
0 files changed, 0 insertions, 0 deletions