From fed2f27b5d23e8dceac1ad8d95b2374d3b72eddf Mon Sep 17 00:00:00 2001
From: filliatr
Date: Wed, 24 Nov 1999 10:48:23 +0000
Subject: Vernacinterp et Vernacentries (partiellement)

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@133 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 proofs/tacinterp.mli | 2 ++
 1 file changed, 2 insertions(+)

(limited to 'proofs')

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
-- 
cgit v1.2.3