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.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/tactics/term_dnet.ml b/tactics/term_dnet.ml
index 6294f9fdc..38342b64d 100644
--- a/tactics/term_dnet.ml
+++ b/tactics/term_dnet.ml
@@ -355,7 +355,7 @@ struct
with Invalid_argument _ -> [],c_id in
let wc,whole_c = if Opt.direction then whole_c,wc else wc,whole_c in
try
- let _ = Termops.filtering ctx Reduction.CUMUL wc whole_c in
+ let _ = Termops.filtering Evd.empty ctx Reduction.CUMUL wc whole_c in
id :: acc
with Termops.CannotFilter -> (* msgnl(str"recon "++Termops.print_constr_env (Global.env()) wc); *) acc
) (TDnet.find_match dpat dn) []