diff options
| author | Emilio Jesus Gallego Arias | 2019-04-05 02:30:45 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2019-04-05 15:05:53 +0200 |
| commit | 54fdae0929f2a05a89cd5c463b9a739ab2e239b8 (patch) | |
| tree | 80c38984687249bba8a66e24ad04a48de80c2bfa /proofs/proof.mli | |
| parent | 3c06ce8dc3a95e5dfe3a4c0a9acdc7dd5dac75cb (diff) | |
[api] [proofs] Remove dependency of proofs on interp.
We perform some cleanup and remove dependency of `proofs/` on
`interp/`, which seems logical.
In fact, `interp` + `parsing` are quite self-contained, so if there is
interest we could also make tactics to depend directly on proofs.
Diffstat (limited to 'proofs/proof.mli')
| -rw-r--r-- | proofs/proof.mli | 7 |
1 files changed, 5 insertions, 2 deletions
diff --git a/proofs/proof.mli b/proofs/proof.mli index 40e8ff7eef..defef57a8d 100644 --- a/proofs/proof.mli +++ b/proofs/proof.mli @@ -249,8 +249,11 @@ module V82 : sig val grab_evars : t -> t (* Implements the Existential command *) - val instantiate_evar : - Environ.env -> int -> Constrexpr.constr_expr -> t -> t + val instantiate_evar + : Environ.env + -> int + -> (Environ.env -> Evd.evar_map -> Glob_term.glob_constr) + -> t -> t end (* returns the set of all goals in the proof *) |