diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-11-24 15:50:17 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-02-14 17:30:38 +0100 |
| commit | b36adb2124d3ba8a5547605e7f89bb0835d0ab10 (patch) | |
| tree | 4ab6481d8d182f6bb3dd241b7112a3027aa26b2a /tactics/term_dnet.ml | |
| parent | ffb59901f568351401f2f3d1f3334031658b8880 (diff) | |
Removing some return type compatibility layers in Termops.
Diffstat (limited to 'tactics/term_dnet.ml')
| -rw-r--r-- | tactics/term_dnet.ml | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/tactics/term_dnet.ml b/tactics/term_dnet.ml index 38342b64d..219abb7fd 100644 --- a/tactics/term_dnet.ml +++ b/tactics/term_dnet.ml @@ -350,9 +350,11 @@ struct TDnet.Idset.fold (fun id acc -> 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) (EConstr.of_constr c_id) (** FIXME *) + try Termops.align_prod_letin Evd.empty (EConstr.of_constr 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 |