diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2015-10-20 16:12:39 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2015-10-20 16:28:52 +0200 |
| commit | 2d747797c427818cdf85d0a0d701c7c9b0106b82 (patch) | |
| tree | fe2a13b39348723dc7a4567198da190650cce2d4 /proofs/tacmach.mli | |
| parent | 4cc1714ac9b0944b6203c23af8c46145e7239ad3 (diff) | |
Proofview.Goal.sigma returns an indexed evarmap.
Diffstat (limited to 'proofs/tacmach.mli')
| -rw-r--r-- | proofs/tacmach.mli | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli index 3ed6a2eeb..c45fd250c 100644 --- a/proofs/tacmach.mli +++ b/proofs/tacmach.mli @@ -111,6 +111,7 @@ module New : sig (** FIXME: encapsulate the level in an existential type. *) val of_old : (Proof_type.goal Evd.sigma -> 'a) -> ([ `NF ], 'r) Proofview.Goal.t -> 'a + val project : ('a, 'r) Proofview.Goal.t -> Evd.evar_map val pf_env : ('a, 'r) Proofview.Goal.t -> Environ.env val pf_concl : ([ `NF ], 'r) Proofview.Goal.t -> types |