diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2014-10-03 17:39:23 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2014-10-03 17:54:38 +0200 |
| commit | c090d3511eaabe205febc68484b7b0738b403310 (patch) | |
| tree | 085c85ac7dc7fb788d811ee9460bffbcaf476e23 /toplevel | |
| parent | 09caa43ae43c0774ea24abb803990d3e70fdc879 (diff) | |
Fixing #3193 (honoring implicit arguments in local definitions).
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/command.ml | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/toplevel/command.ml b/toplevel/command.ml index a23b1b64a..fb73c5aa8 100644 --- a/toplevel/command.ml +++ b/toplevel/command.ml @@ -158,12 +158,14 @@ let declare_definition ident (local, p, k) ce imps hook = let c = SectionLocalDef ce in let _ = declare_variable ident (Lib.cwd(), c, IsDefinition k) in let () = definition_message ident in + let gr = VarRef ident in + let () = maybe_declare_manual_implicits false gr imps in let () = if Pfedit.refining () then let msg = strbrk "Section definition " ++ pr_id ident ++ strbrk " is not visible from current goals" in msg_warning msg in - VarRef ident + gr | Discharge | Local | Global -> declare_global_definition ident ce local k imps in Lemmas.call_hook (Future.fix_exn_of ce.Entries.const_entry_body) hook local r |