diff options
Diffstat (limited to 'proofs')
| -rw-r--r-- | proofs/tacinterp.mli | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/proofs/tacinterp.mli b/proofs/tacinterp.mli index 5dbad51769..aa71f411dc 100644 --- a/proofs/tacinterp.mli +++ b/proofs/tacinterp.mli @@ -11,6 +11,8 @@ open Term (* Interpretation of tactics. *) +val cvt_arg : Coqast.t -> tactic_arg + val tacinterp_add : string * (tactic_arg list -> tactic) -> unit val tacinterp_map : string -> tactic_arg list -> tactic val tacinterp_init : unit -> unit |