From 20cfd67c4965454cfc7070887eb85c2a2ff11ca2 Mon Sep 17 00:00:00 2001
From: SimonBoulier
Date: Tue, 28 Jan 2020 15:08:48 +0100
Subject: Correct bug in non max local implicit arguments

+ tests in the test-suite for non max local implicit arguments
---
 interp/constrintern.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'interp')

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
-- 
cgit v1.2.3