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
|
(************************************************************************)
(* * 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) *)
(************************************************************************)
val check_evars : Environ.env -> Evd.evar_map -> unit
type obligation_info =
( Names.Id.t
* Constr.types
* Evar_kinds.t Loc.located
* (bool * Evar_kinds.obligation_definition_status)
* Int.Set.t
* unit Proofview.tactic option )
array
(** ident, type, location of the original evar, (opaque or
transparent, expand or define), dependencies as indexes into the
array, tactic to solve it *)
val retrieve_obligations :
Environ.env
-> Names.Id.t
-> Evd.evar_map
-> int
-> ?status:Evar_kinds.obligation_definition_status
-> EConstr.t
-> EConstr.types
-> obligation_info
* ( (Evar.t * Names.Id.t) list
* ((Names.Id.t -> EConstr.t) -> EConstr.t -> Constr.t) )
* Constr.t
* Constr.t
(** [retrieve_obligations env id sigma fs ?status body type] returns
[obls, (evnames, evmap), nbody, ntype] a list of obligations built
from evars in [body, type].
[fs] is the number of function prototypes to try to clear from
evars contexts. [evnames, evmap) is the list of names /
substitution functions used to program with holes. This is not used
in Coq, but in the equations plugin; [evnames] is actually
redundant with the information contained in [obls] *)
|
