diff options
Diffstat (limited to 'tactics/equality.ml')
| -rw-r--r-- | tactics/equality.ml | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/tactics/equality.ml b/tactics/equality.ml index ba982ccee..5212711ae 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -116,12 +116,13 @@ let general_rewrite_ebindings_clause cls lft2rgt occs (c,l) with_evars gl = let ctype = pf_apply get_type_of gl c in let env = pf_env gl in let sigma = project gl in - let t = snd (decompose_prod (whd_betaiotazeta ctype)) in + let rels, t = decompose_prod (whd_betaiotazeta ctype) in match match_with_equation t with | Some (hdcncl,_) -> (* Fast path: direct leibniz rewrite *) leibniz_rewrite_ebindings_clause cls lft2rgt (c,l) with_evars gl hdcncl | None -> - let _,t' = splay_prod env sigma t in (* Search for underlying eq *) + 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 | Some (hdcncl,_) -> (* Maybe a setoid relation with eq inside *) if l = NoBindings && !is_applied_setoid_relation t then |