diff options
Diffstat (limited to 'tactics/equality.ml')
| -rw-r--r-- | tactics/equality.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/tactics/equality.ml b/tactics/equality.ml index cbcf5993c..641e274af 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -116,13 +116,13 @@ let general_rewrite_ebindings_clause cls lft2rgt occs ((c,l) : open_constr with_ let sigma = Evd.merge sigma (project gl) in let ctype = get_type_of env sigma c' in let rels, t = decompose_prod (whd_betaiotazeta ctype) in - match match_with_equation t with + match match_with_equality_type t with | Some (hdcncl,_) -> (* Fast path: direct leibniz rewrite *) leibniz_rewrite_ebindings_clause cls lft2rgt sigma c' l with_evars gl hdcncl | None -> let env' = List.fold_left (fun env (n,t) -> push_rel (n, None, t) env) env rels in let _,t' = splay_prod env' sigma t in (* Search for underlying eq *) - match match_with_equation t' with + match match_with_equality_type t' with | Some (hdcncl,_) -> (* Maybe a setoid relation with eq inside *) if l = NoBindings && !is_applied_setoid_relation t then !general_setoid_rewrite_clause cls lft2rgt occs c ~new_goals:[] gl |