From a1d00fa77939f99dd5e7ddd41c8ecf64e8af4fa1 Mon Sep 17 00:00:00 2001
From: SimonBoulier
Date: Mon, 2 Dec 2019 12:52:39 +0100
Subject: Add syntax for non maximally inserted implicit arguments

---
 vernac/comAssumption.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'vernac/comAssumption.ml')

diff --git a/vernac/comAssumption.ml b/vernac/comAssumption.ml
index 625ffb5a06..d97bf6724c 100644
--- a/vernac/comAssumption.ml
+++ b/vernac/comAssumption.ml
@@ -270,7 +270,7 @@ let context ~poly l =
         | Some (Name id',_) -> Id.equal name id'
         | _ -> false
       in
-      let impl = Glob_term.(if List.exists test impls then Implicit else 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