From fd4bc8cefc7ae2724d9c386ecfeda2e2feccd98c Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Thu, 2 Jul 2020 15:07:39 +0200
Subject: Fix Context with nonmaximplicit.

Fix #12551
---
 vernac/comAssumption.ml | 11 +++++++----
 1 file changed, 7 insertions(+), 4 deletions(-)

(limited to 'vernac')

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