diff options
| author | Enrico Tassi | 2016-02-02 09:46:08 +0100 |
|---|---|---|
| committer | Enrico Tassi | 2016-02-02 09:46:08 +0100 |
| commit | 371abe046a33c2728275dbe1e3d8dc721aa4dd94 (patch) | |
| tree | 1f1b615a8ccf0ef8e0c295e1d4e98d0bde566ccc /mathcomp/ssreflect/plugin | |
| parent | 25d7e5b7392afb4ef48e7d0e563b8a2f7851823a (diff) | |
fix debug print
Diffstat (limited to 'mathcomp/ssreflect/plugin')
| -rw-r--r-- | mathcomp/ssreflect/plugin/trunk/ssreflect.ml4 | 2 | ||||
| -rw-r--r-- | mathcomp/ssreflect/plugin/v8.5/ssreflect.ml4 | 2 |
2 files changed, 2 insertions, 2 deletions
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 |