From 9024a91b59b9ecfb94e68b3748f2a9a66adcf515 Mon Sep 17 00:00:00 2001
From: ppedrot
Date: Fri, 21 Jun 2013 12:36:19 +0000
Subject: Cutting the dependency of Genarg in constr_expr, glob_constr related
 types. This will ultimately allow putting genargs into these ASTs.

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

(limited to 'proofs')

diff --git a/proofs/tactic_debug.mli b/proofs/tactic_debug.mli
index a9cd025a7f..3b9858f16e 100644
--- a/proofs/tactic_debug.mli
+++ b/proofs/tactic_debug.mli
@@ -22,7 +22,7 @@ val tactic_printer : (glob_tactic_expr -> Pp.std_ppcmds) Hook.t
 val match_pattern_printer :
   (env -> constr_pattern match_pattern -> Pp.std_ppcmds) Hook.t
 val match_rule_printer :
-  ((Genarg.glob_constr_and_expr * constr_pattern,glob_tactic_expr) match_rule -> Pp.std_ppcmds) Hook.t
+  ((Tacexpr.glob_constr_and_expr * constr_pattern,glob_tactic_expr) match_rule -> Pp.std_ppcmds) Hook.t
 
 (** Debug information *)
 type debug_info =
@@ -41,7 +41,7 @@ val db_constr : debug_info -> env -> constr -> unit
 
 (** Prints the pattern rule *)
 val db_pattern_rule :
-  debug_info -> int -> (Genarg.glob_constr_and_expr * constr_pattern,glob_tactic_expr) match_rule -> unit
+  debug_info -> int -> (Tacexpr.glob_constr_and_expr * constr_pattern,glob_tactic_expr) match_rule -> unit
 
 (** Prints a matched hypothesis *)
 val db_matched_hyp :
-- 
cgit v1.2.3