From c5e2f573ef079800eed4c8246c4f2bd39bf47b26 Mon Sep 17 00:00:00 2001
From: Jasper Hugunin
Date: Sat, 19 Jan 2019 18:20:36 -0800
Subject: Apply implicit binders to Hypothesis inside sections.

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

(limited to 'vernac/comAssumption.ml')

diff --git a/vernac/comAssumption.ml b/vernac/comAssumption.ml
index 4fb06e4e09..35d8be5c56 100644
--- a/vernac/comAssumption.ml
+++ b/vernac/comAssumption.ml
@@ -57,6 +57,7 @@ match local with
     strbrk " is not visible from current goals")
   in
   let r = VarRef ident in
+  let () = maybe_declare_manual_implicits true r imps in
   let () = Typeclasses.declare_instance None true r in
   let () = if is_coe then Class.try_add_new_coercion r ~local:true false in
   (r,Univ.Instance.empty,true)
-- 
cgit v1.2.3