Merge PR #12626: Fix Context with nonmaximplicit.

Reviewed-by: ejgallego

2 files changed, 15 insertions, 4 deletions

diff --git a/test-suite/bugs/closed/bug_12551.v b/test-suite/bugs/closed/bug_12551.v
new file mode 100644
index 0000000000..77ecb367ec
--- /dev/null
+++ b/test-suite/bugs/closed/bug_12551.v
@@ -0,0 +1,8 @@
+
+Section S.
+  Context [A:Type] (a:A).
+  Definition id := a.
+End S.
+
+Check id : forall A, A -> A.
+Check id 0 : nat.
diff --git a/vernac/comAssumption.ml b/vernac/comAssumption.ml
index d8475126ca..401ba0fba4 100644
--- a/vernac/comAssumption.ml
+++ b/vernac/comAssumption.ml
@@ -268,11 +268,14 @@ let context ~poly l =
       in
       let b = Option.map (EConstr.to_constr sigma) b in
       let t = EConstr.to_constr sigma t in
-      let test x = match x.CAst.v with
-        | Some (Name id',_) -> Id.equal name id'
-        | _ -> false
+      let impl = let open Glob_term in
+      let search x = match x.CAst.v with
+        | Some (Name id',max) when Id.equal name id' ->
+          Some (if max then MaxImplicit else NonMaxImplicit)
+        | _ -> None
+        in
+        try CList.find_map search impls with Not_found -> Explicit
       in
-      let impl = Glob_term.(if List.exists test impls then MaxImplicit else Explicit) in (* ??? *)
       name,b,t,impl)
       ctx
   in