diff options
Diffstat (limited to 'tactics/hipattern.ml')
| -rw-r--r-- | tactics/hipattern.ml | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/tactics/hipattern.ml b/tactics/hipattern.ml index 6681e5e491..36ed589b99 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 = |