From 05afd04095e35d77ca135bd2c1cb8d303ea2d6a8 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Thu, 24 Nov 2016 18:18:17 +0100
Subject: Ltac now uses evar-based constrs.

---
 ltac/tactic_debug.mli | 7 ++++---
 1 file changed, 4 insertions(+), 3 deletions(-)

(limited to 'ltac/tactic_debug.mli')

diff --git a/ltac/tactic_debug.mli b/ltac/tactic_debug.mli
index 520fb41eff..7745d9b7b6 100644
--- a/ltac/tactic_debug.mli
+++ b/ltac/tactic_debug.mli
@@ -11,6 +11,7 @@ open Pattern
 open Names
 open Tacexpr
 open Term
+open EConstr
 open Evd
 
 (** TODO: Move those definitions somewhere sensible *)
@@ -34,7 +35,7 @@ val debug_prompt :
 val db_initialize : unit Proofview.NonLogical.t
 
 (** Prints a constr *)
-val db_constr : debug_info -> env -> constr -> unit Proofview.NonLogical.t
+val db_constr : debug_info -> env -> evar_map -> constr -> unit Proofview.NonLogical.t
 
 (** Prints the pattern rule *)
 val db_pattern_rule :
@@ -42,10 +43,10 @@ val db_pattern_rule :
 
 (** Prints a matched hypothesis *)
 val db_matched_hyp :
-  debug_info -> env -> Id.t * constr option * constr -> Name.t -> unit Proofview.NonLogical.t
+  debug_info -> env -> evar_map -> Id.t * constr option * constr -> Name.t -> unit Proofview.NonLogical.t
 
 (** Prints the matched conclusion *)
-val db_matched_concl : debug_info -> env -> constr -> unit Proofview.NonLogical.t
+val db_matched_concl : debug_info -> env -> evar_map -> constr -> unit Proofview.NonLogical.t
 
 (** Prints a success message when the goal has been matched *)
 val db_mc_pattern_success : debug_info -> unit Proofview.NonLogical.t
-- 
cgit v1.2.3