diff options
| author | Pierre Boutillier | 2014-04-02 11:22:21 +0200 |
|---|---|---|
| committer | Pierre Boutillier | 2014-04-02 11:23:25 +0200 |
| commit | c3feef4ed5dec126f1144dec91eee9c0f0522a94 (patch) | |
| tree | 478f1c004e87cdd18e92766ddbc47767d231f36a /kernel/nativecode.ml | |
| parent | f963cf312d5a8ebb84af92489be5efd49fe6f434 (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/nativecode.ml')
0 files changed, 0 insertions, 0 deletions