diff options
| author | Jasper Hugunin | 2019-01-19 18:20:36 -0800 |
|---|---|---|
| committer | Jasper Hugunin | 2019-02-22 10:28:45 -0800 |
| commit | c5e2f573ef079800eed4c8246c4f2bd39bf47b26 (patch) | |
| tree | c581b1ab6052bea7921b258070292140967b4ab6 /vernac/comAssumption.ml | |
| parent | 6a289e4fbc1c4327429bb7041e8f39a18bbb0f70 (diff) | |
Apply implicit binders to Hypothesis inside sections.
Diffstat (limited to 'vernac/comAssumption.ml')
| -rw-r--r-- | vernac/comAssumption.ml | 1 |
1 files changed, 1 insertions, 0 deletions
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) |