From 371abe046a33c2728275dbe1e3d8dc721aa4dd94 Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Tue, 2 Feb 2016 09:46:08 +0100
Subject: fix debug print

---
 mathcomp/ssreflect/plugin/trunk/ssreflect.ml4 | 2 +-
 mathcomp/ssreflect/plugin/v8.5/ssreflect.ml4  | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

(limited to 'mathcomp/ssreflect/plugin')

diff --git a/mathcomp/ssreflect/plugin/trunk/ssreflect.ml4 b/mathcomp/ssreflect/plugin/trunk/ssreflect.ml4
index d4f1b21..72efb36 100644
--- a/mathcomp/ssreflect/plugin/trunk/ssreflect.ml4
+++ b/mathcomp/ssreflect/plugin/trunk/ssreflect.ml4
@@ -4965,7 +4965,7 @@ let rwprocess_rule dir rule gl =
       let t =
         if red = 1 then Tacred.hnf_constr env sigma t0
         else Reductionops.whd_betaiotazeta sigma t0 in
-      pp(lazy(str"rewrule="++pr_constr t));
+      pp(lazy(str"rewrule="++pr_constr_pat t));
       match kind_of_term t with
       | Prod (_, xt, at) ->
         let sigma = create_evar_defs sigma in
diff --git a/mathcomp/ssreflect/plugin/v8.5/ssreflect.ml4 b/mathcomp/ssreflect/plugin/v8.5/ssreflect.ml4
index 06c6a6c..eb21fc2 100644
--- a/mathcomp/ssreflect/plugin/v8.5/ssreflect.ml4
+++ b/mathcomp/ssreflect/plugin/v8.5/ssreflect.ml4
@@ -4919,7 +4919,7 @@ let rwprocess_rule dir rule gl =
       let t =
         if red = 1 then Tacred.hnf_constr env sigma t0
         else Reductionops.whd_betaiotazeta sigma t0 in
-      pp(lazy(str"rewrule="++pr_constr t));
+      pp(lazy(str"rewrule="++pr_constr_pat t));
       match kind_of_term t with
       | Prod (_, xt, at) ->
         let ise, x = Evarutil.new_evar env (create_evar_defs sigma) xt in
-- 
cgit v1.2.3