Now glob_sign and interp_sign only depend on structures defined

upto Genarg, so moved them there. This will allow defining the new
genarg interface.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16584 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 1 insertions, 1 deletions

diff --git a/tactics/tacintern.mli b/tactics/tacintern.mli
index c928b7379..75576516f 100644
--- a/tactics/tacintern.mli
+++ b/tactics/tacintern.mli
@@ -23,7 +23,7 @@ open Nametab
 (** Globalization of tactic expressions :
     Conversion from [raw_tactic_expr] to [glob_tactic_expr] *)
 
-type glob_sign = {
+type glob_sign = Genarg.glob_sign = {
   ltacvars : Id.t list * Id.t list;
   ltacrecvars : (Id.t * ltac_constant) list;
   gsigma : Evd.evar_map;