From b4b90c5d2e8c413e1981c456c933f35679386f09 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Sat, 26 Nov 2016 16:18:47 +0100 Subject: Definining EConstr-based contexts. This removes quite a few unsafe casts. Unluckily, I had to reintroduce the old non-module based names for these data structures, because I could not reproduce easily the same hierarchy in EConstr. --- tactics/term_dnet.ml | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) (limited to 'tactics/term_dnet.ml') 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 -- cgit v1.2.3