diff options
| author | Emilio Jesus Gallego Arias | 2019-05-21 16:48:03 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2019-05-21 16:48:03 +0200 |
| commit | e9a5fe993ba36e22316ac9f6ef0564f38a3eb4f9 (patch) | |
| tree | 0ffb42301743171b24d6bb0c4205eba78e889e50 /vernac/declareDef.ml | |
| parent | 0aa9a5407874332dfa31f1a0f73d2dc91e95fb39 (diff) | |
| parent | f6751f5e8aae4f37d302f700d2f5f2e9fba73a1e (diff) | |
Merge PR #10188: Remove definition-not-visible warning
Reviewed-by: gares
Diffstat (limited to 'vernac/declareDef.ml')
| -rw-r--r-- | vernac/declareDef.ml | 13 |
1 files changed, 3 insertions, 10 deletions
diff --git a/vernac/declareDef.ml b/vernac/declareDef.ml index 052832244b..bdda3314ca 100644 --- a/vernac/declareDef.ml +++ b/vernac/declareDef.ml @@ -14,12 +14,6 @@ open Entries open Globnames open Impargs -let warn_definition_not_visible = - CWarnings.create ~name:"definition-not-visible" ~category:"implicits" - Pp.(fun ident -> - strbrk "Section definition " ++ - Names.Id.print ident ++ strbrk " is not visible from current goals") - let warn_local_declaration = CWarnings.create ~name:"local-declaration" ~category:"scope" Pp.(fun (id,kind) -> @@ -33,12 +27,11 @@ let get_locality id ~kind = function | Local -> true | Global -> false -let declare_definition ~ontop ident (local, p, k) ?hook_data ce pl imps = +let declare_definition ident (local, p, k) ?hook_data ce pl imps = let fix_exn = Future.fix_exn_of ce.const_entry_body in let gr = match local with | Discharge when Lib.sections_are_opened () -> let _ = declare_variable ident (Lib.cwd(), SectionLocalDef ce, IsDefinition k) in - let () = if Option.has_some ontop then warn_definition_not_visible ident in VarRef ident | Discharge | Local | Global -> let local = get_locality ident ~kind:"definition" local in @@ -57,9 +50,9 @@ let declare_definition ~ontop ident (local, p, k) ?hook_data ce pl imps = end; gr -let declare_fix ~ontop ?(opaque = false) ?hook_data (_,poly,_ as kind) pl univs f ((def,_),eff) t imps = +let declare_fix ?(opaque = false) ?hook_data (_,poly,_ as kind) pl univs f ((def,_),eff) t imps = let ce = definition_entry ~opaque ~types:t ~univs ~eff def in - declare_definition ~ontop f kind ?hook_data ce pl imps + declare_definition f kind ?hook_data ce pl imps let check_definition_evars ~allow_evars sigma = let env = Global.env () in |