blob: 7d8a112cc671b79ec6c8fd16bb74a953bdc3b413 (
plain)
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
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
|
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
(* <O___,, * (see CREDITS file for the list of authors) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(* * (see LICENSE file for the text of the license) *)
(************************************************************************)
open Names
open Constr
type 'a obligation_body = DefinedObl of 'a | TermObl of constr
type obligation =
{ obl_name : Id.t
; obl_type : types
; obl_location : Evar_kinds.t Loc.located
; obl_body : pconstant obligation_body option
; obl_status : bool * Evar_kinds.obligation_definition_status
; obl_deps : Int.Set.t
; obl_tac : unit Proofview.tactic option }
type obligations = obligation array * int
type fixpoint_kind =
| IsFixpoint of lident option list
| IsCoFixpoint
type program_info =
{ prg_name : Id.t
; prg_body : constr
; prg_type : constr
; prg_ctx : UState.t
; prg_univdecl : UState.universe_decl
; prg_obligations : obligations
; prg_deps : Id.t list
; prg_fixkind : fixpoint_kind option
; prg_implicits : Impargs.manual_implicits
; prg_notations : Vernacexpr.decl_notation list
; prg_poly : bool
; prg_scope : DeclareDef.locality
; prg_kind : Decls.definition_object_kind
; prg_reduce : constr -> constr
; prg_hook : DeclareDef.Hook.t option
; prg_opaque : bool
}
val declare_obligation :
program_info
-> obligation
-> Constr.types
-> Constr.types option
-> Entries.universes_entry
-> bool * obligation
(** [declare_obligation] Save an obligation *)
module ProgMap : CMap.ExtS with type key = Id.t and module Set := Id.Set
val declare_definition : program_info -> Names.GlobRef.t
type progress =
(* Resolution status of a program *)
| Remain of int
(* n obligations remaining *)
| Dependent
(* Dependent on other definitions *)
| Defined of GlobRef.t
(* Defined as id *)
type obligation_qed_info =
{ name : Id.t
; num : int
; auto : Id.t option -> Int.Set.t -> unit Proofview.tactic option -> progress
}
val obligation_terminator
: Evd.side_effects Declare.proof_entry list
-> UState.t
-> obligation_qed_info -> unit
(** [obligation_terminator] part 2 of saving an obligation *)
val update_obls :
program_info
-> obligation array
-> int
-> progress
(** [update_obls prg obls n progress] What does this do? *)
(** { 2 Util } *)
val get_prg_info_map : unit -> program_info CEphemeron.key ProgMap.t
val program_tcc_summary_tag :
program_info CEphemeron.key Id.Map.t Summary.Dyn.tag
val obl_substitution :
bool
-> obligation array
-> Int.Set.t
-> (ProgMap.key * (Constr.types * Constr.types)) list
val dependencies : obligation array -> int -> Int.Set.t
val err_not_transp : unit -> unit
val progmap_add : ProgMap.key -> program_info CEphemeron.key -> unit
(* This is a hack to make it possible for Obligations to craft a Qed
* behind the scenes. The fix_exn the Stm attaches to the Future proof
* is not available here, so we provide a side channel to get it *)
val stm_get_fix_exn : (unit -> Exninfo.iexn -> Exninfo.iexn) Hook.t
|
