aboutsummaryrefslogtreecommitdiff
path: root/kernel
diff options
context:
space:
mode:
authorPierre Boutillier2014-04-02 11:22:21 +0200
committerPierre Boutillier2014-04-02 11:23:25 +0200
commitc3feef4ed5dec126f1144dec91eee9c0f0522a94 (patch)
tree478f1c004e87cdd18e92766ddbc47767d231f36a /kernel
parentf963cf312d5a8ebb84af92489be5efd49fe6f434 (diff)
Fix Bug 3217
Normalize the term to see if there are arguments to daclare implicits only if at least one argument occurs in the non normal form
Diffstat (limited to 'kernel')
0 files changed, 0 insertions, 0 deletions