diff options
Diffstat (limited to 'proofs/proof_trees.mli')
| -rw-r--r-- | proofs/proof_trees.mli | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/proofs/proof_trees.mli b/proofs/proof_trees.mli index 9730652f52..c2b73c85d4 100644 --- a/proofs/proof_trees.mli +++ b/proofs/proof_trees.mli @@ -86,4 +86,5 @@ val pr_evars : (int * goal) list -> std_ppcmds val pr_evars_int : int -> (int * goal) list -> std_ppcmds val pr_subgoals_existential : enamed_declarations -> goal list -> std_ppcmds +(* Gives the ast corresponding to a tactic argument *) val ast_of_cvt_arg : tactic_arg -> Coqast.t |