diff options
Diffstat (limited to 'proofs/pfedit.mli')
| -rw-r--r-- | proofs/pfedit.mli | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/proofs/pfedit.mli b/proofs/pfedit.mli index dde52d0cc..c16445ba3 100644 --- a/proofs/pfedit.mli +++ b/proofs/pfedit.mli @@ -180,6 +180,6 @@ val instantiate_nth_evar_com : int -> Topconstr.constr_expr -> unit (** [build_by_tactic typ tac] returns a term of type [typ] by calling [tac] *) -val build_constant_by_tactic : named_context_val -> types -> tactic -> +val build_constant_by_tactic : identifier -> named_context_val -> types -> tactic -> Entries.definition_entry val build_by_tactic : types -> tactic -> constr |