diff options
Diffstat (limited to 'proofs/proofview.mli')
| -rw-r--r-- | proofs/proofview.mli | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/proofs/proofview.mli b/proofs/proofview.mli index fe24b54b3..1ae5c4fd2 100644 --- a/proofs/proofview.mli +++ b/proofs/proofview.mli @@ -210,7 +210,7 @@ module V82 : sig val top_evars : proofview -> Evd.evar list (* Implements the Existential command *) - val instantiate_evar : int -> Topconstr.constr_expr -> proofview -> proofview + val instantiate_evar : int -> Constrexpr.constr_expr -> proofview -> proofview (* spiwack: [purify] might be useful while writing tactics manipulating exception explicitely or from the [V82] submodule (neither being advised, though *) |