aboutsummaryrefslogtreecommitdiff
path: root/proofs/pfedit.mli
diff options
context:
space:
mode:
Diffstat (limited to 'proofs/pfedit.mli')
-rw-r--r--proofs/pfedit.mli2
1 files changed, 1 insertions, 1 deletions
diff --git a/proofs/pfedit.mli b/proofs/pfedit.mli
index 4ca23e7116..73850c6f07 100644
--- a/proofs/pfedit.mli
+++ b/proofs/pfedit.mli
@@ -174,4 +174,4 @@ val build_by_tactic : env -> types -> tactic -> constr
val declare_implicit_tactic : tactic -> unit
(* Raise Exit if cannot solve *)
-val solve_by_implicit_tactic : env -> Evd.evar_map -> existential -> constr
+val solve_by_implicit_tactic : env -> Evd.evar_map -> Evd.evar -> constr