diff options
| author | Maxime Dénès | 2017-06-15 11:52:19 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2017-06-15 11:52:19 +0200 |
| commit | 28c732ea340f5ac571a77a8ac26de600c29165b2 (patch) | |
| tree | 9ee6deb6ecb31c520ffb4c278560a527cb550db4 /interp | |
| parent | e710306910afc61c9a874e6020bbf35b77ffe4af (diff) | |
| parent | 7668037a8daaef7bc8f1fc3225c2e6cc26cac0aa (diff) | |
Merge PR#375: Deprecation
Diffstat (limited to 'interp')
| -rw-r--r-- | interp/constrintern.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 3d484a02da..67fee62028 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -786,7 +786,7 @@ let find_appl_head_data c = let scopes = find_arguments_scope ref in c, impls, scopes, [] | GApp ({ v = GRef (ref,_) },l) - when l != [] && Flags.version_strictly_greater Flags.V8_2 -> + when l != [] -> let n = List.length l in let impls = implicits_of_global ref in let scopes = find_arguments_scope ref in |