diff options
| author | Talia Ringer | 2019-05-22 16:09:51 -0400 |
|---|---|---|
| committer | Talia Ringer | 2019-05-22 16:09:51 -0400 |
| commit | 577db38704896c75d1db149f6b71052ef47202be (patch) | |
| tree | 946afdb361fc9baaa696df7891d0ddc03a4a8594 /vernac/declareDef.ml | |
| parent | 7eefc0b1db614158ed1b322f8c6e5601e3995113 (diff) | |
| parent | e9a5fe993ba36e22316ac9f6ef0564f38a3eb4f9 (diff) | |
Merge remote-tracking branch 'origin/master' into stm+doc_hook
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 |