From 451acd6ca6a9ce5b86622fb42085eb19e23d6665 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Mon, 19 Aug 2019 15:20:31 +0200
Subject: [declare] Use `binding_kind` for implicit kind instead of boolean.

---
 vernac/comAssumption.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'vernac/comAssumption.ml')

diff --git a/vernac/comAssumption.ml b/vernac/comAssumption.ml
index 7d365db85c..e3f90ab98c 100644
--- a/vernac/comAssumption.ml
+++ b/vernac/comAssumption.ml
@@ -100,7 +100,7 @@ let next_uctx =
 let declare_assumptions idl is_coe ~scope ~poly ~kind typ uctx pl imps nl =
   let refs, _ =
     List.fold_left (fun (refs,uctx) id ->
-        let ref = declare_assumption is_coe ~scope ~poly ~kind typ uctx pl imps false nl id in
+        let ref = declare_assumption is_coe ~scope ~poly ~kind typ uctx pl imps Glob_term.Explicit nl id in
         ref::refs, next_uctx uctx)
       ([],uctx) idl
   in
@@ -292,7 +292,7 @@ let context ~poly l =
         | Some (Name id',_) -> Id.equal name id'
         | _ -> false
       in
-      let impl = List.exists test impls in
+      let impl = if List.exists test impls then Glob_term.Implicit else Glob_term.Explicit in
       let scope =
         if Lib.sections_are_opened () then DeclareDef.Discharge else DeclareDef.Global ImportDefaultBehavior in
       match b with
-- 
cgit v1.2.3