From db252cb87e9c63f400fd4fddd2d771df3160d592 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Sat, 19 Nov 2016 01:07:35 +0100 Subject: Inv API using EConstr. --- tactics/hipattern.ml | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) (limited to 'tactics/hipattern.ml') diff --git a/tactics/hipattern.ml b/tactics/hipattern.ml index 6681e5e49..36ed589b9 100644 --- a/tactics/hipattern.ml +++ b/tactics/hipattern.ml @@ -470,10 +470,11 @@ let match_eq_nf gls eqn (ref, hetero) = let n = if hetero then 4 else 3 in let args = List.init n (fun i -> mkGPatVar ("X" ^ string_of_int (i + 1))) in let pat = mkPattern (mkGAppRef ref args) in + let pf_whd_all gls c = EConstr.of_constr (pf_whd_all gls (EConstr.of_constr c)) in match Id.Map.bindings (pf_matches gls pat eqn) with | [(m1,t);(m2,x);(m3,y)] -> assert (Id.equal m1 meta1 && Id.equal m2 meta2 && Id.equal m3 meta3); - (t,pf_whd_all gls (EConstr.of_constr x),pf_whd_all gls (EConstr.of_constr y)) + (EConstr.of_constr t,pf_whd_all gls x,pf_whd_all gls y) | _ -> anomaly ~label:"match_eq" (Pp.str "an eq pattern should match 3 terms") let dest_nf_eq gls eqn = -- cgit v1.2.3