aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite
diff options
context:
space:
mode:
authorGravatar Pierre Boutillier <pierre.boutillier@ens-lyon.org>2014-04-02 11:22:21 +0200
committerGravatar Pierre Boutillier <pierre.boutillier@ens-lyon.org>2014-04-02 11:23:25 +0200
commitc3feef4ed5dec126f1144dec91eee9c0f0522a94 (patch)
tree478f1c004e87cdd18e92766ddbc47767d231f36a /test-suite
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 'test-suite')
0 files changed, 0 insertions, 0 deletions