diff options
Diffstat (limited to 'tactics/term_dnet.ml')
| -rw-r--r-- | tactics/term_dnet.ml | 5 |
1 files changed, 2 insertions, 3 deletions
diff --git a/tactics/term_dnet.ml b/tactics/term_dnet.ml index 219abb7fd..2c863c42a 100644 --- a/tactics/term_dnet.ml +++ b/tactics/term_dnet.ml @@ -344,7 +344,7 @@ struct ) (pr_dconstr pr_term_pattern) p*) let search_pat cpat dpat dn = - let whole_c = cpat in + let whole_c = EConstr.of_constr cpat in (* if we are at the root, add an empty context *) let dpat = under_prod (empty_ctx dpat) in TDnet.Idset.fold @@ -352,9 +352,8 @@ struct let c_id = Opt.reduce (Ident.constr_of id) in let c_id = EConstr.of_constr c_id in let (ctx,wc) = - try Termops.align_prod_letin Evd.empty (EConstr.of_constr whole_c) c_id (** FIXME *) + try Termops.align_prod_letin Evd.empty whole_c c_id (** FIXME *) with Invalid_argument _ -> [],c_id in - let wc = EConstr.Unsafe.to_constr wc in let wc,whole_c = if Opt.direction then whole_c,wc else wc,whole_c in try let _ = Termops.filtering Evd.empty ctx Reduction.CUMUL wc whole_c in |