vernac/declareDef.ml

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63

(************************************************************************)
(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017     *)
(*   \VV/  **************************************************************)
(*    //   *      This file is distributed under the terms of the       *)
(*         *       GNU Lesser General Public License Version 2.1        *)
(************************************************************************)

open Decl_kinds
open Declare
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) ->
        Names.Id.print id ++ strbrk " is declared as a local " ++ str kind)

let get_locality id ~kind = function
| Discharge ->
  (** If a Let is defined outside a section, then we consider it as a local definition *)
   warn_local_declaration (id,kind);
  true
| Local -> true
| Global -> false

let declare_global_definition ident ce local k pl imps =
  let local = get_locality ident ~kind:"definition" local in
  let kn = declare_constant ident ~local (DefinitionEntry ce, IsDefinition k) in
  let gr = ConstRef kn in
  let () = maybe_declare_manual_implicits false gr imps in
  let () = Universes.register_universe_binders gr pl in
  let () = definition_message ident in
  gr

let declare_definition ident (local, p, k) ce pl imps hook =
  let fix_exn = Future.fix_exn_of ce.const_entry_body in
  let r = match local with
  | Discharge when Lib.sections_are_opened () ->
    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 Proof_global.there_are_pending_proofs () then
               warn_definition_not_visible ident
    in
    gr
  | Discharge | Local | Global ->
    declare_global_definition ident ce local k pl imps in
  Lemmas.call_hook fix_exn hook local r

let declare_fix ?(opaque = false) (_,poly,_ as kind) pl univs f ((def,_),eff) t imps =
  let ce = definition_entry ~opaque ~types:t ~univs ~eff def in
  declare_definition f kind ce pl imps (Lemmas.mk_hook (fun _ r -> r))