aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics/term_dnet.ml
diff options
context:
space:
mode:
Diffstat (limited to 'tactics/term_dnet.ml')
-rw-r--r--tactics/term_dnet.ml4
1 files changed, 2 insertions, 2 deletions
diff --git a/tactics/term_dnet.ml b/tactics/term_dnet.ml
index e05f4bcfe..f8d7a197b 100644
--- a/tactics/term_dnet.ml
+++ b/tactics/term_dnet.ml
@@ -337,11 +337,11 @@ struct
| _ -> assert false
(* debug *)
- let rec pr_term_pattern p =
+(* let rec pr_term_pattern p =
(fun pr_t -> function
| Term t -> pr_t t
| Meta m -> str"["++Pp.int (Obj.magic m)++str"]"
- ) (pr_dconstr pr_term_pattern) p
+ ) (pr_dconstr pr_term_pattern) p*)
let search_pat cpat dpat dn =
let whole_c = cpat in