diff options
Diffstat (limited to 'proofs/proofview.mli')
| -rw-r--r-- | proofs/proofview.mli | 3 |
1 files changed, 0 insertions, 3 deletions
diff --git a/proofs/proofview.mli b/proofs/proofview.mli index 7f95a053a8..61014468b5 100644 --- a/proofs/proofview.mli +++ b/proofs/proofview.mli @@ -577,9 +577,6 @@ module V82 : sig (* returns the existential variable used to start the proof *) val top_evars : entry -> Evd.evar list - - (* Implements the Existential command *) - val instantiate_evar : int -> Constrexpr.constr_expr -> proofview -> proofview (* Caution: this function loses quite a bit of information. It should be avoided as much as possible. It should work as |