aboutsummaryrefslogtreecommitdiff
path: root/interp
diff options
context:
space:
mode:
Diffstat (limited to 'interp')
-rw-r--r--interp/constrintern.ml4
1 files changed, 2 insertions, 2 deletions
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index ab20f1b3ef..b1e12bd66e 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -335,8 +335,8 @@ let build_impls ?loc n bk na acc =
if exists_name na acc then begin warn_shadowed_implicit_name ?loc na; Anonymous end
else na in
let impl = match na with
- | Name id -> Some (ExplByName id,Manual,(true,true))
- | Anonymous -> Some (ExplByPos (n,None),Manual,(true,true)) in
+ | Name id -> Some (ExplByName id,Manual,(max,true))
+ | Anonymous -> Some (ExplByPos (n,None),Manual,(max,true)) in
impl
in
match bk with