Procedural: some improvements

[helm.git] / components / tactics / equalityTactics.ml

diff --git a/components/tactics/equalityTactics.ml b/components/tactics/equalityTactics.ml
index f2760c30f33f394daded905bc246cc63446e7321..b445dfb868d8d354aeaafb6ad303c43830de5865 100644 (file)
--- a/components/tactics/equalityTactics.ml
+++ b/components/tactics/equalityTactics.ml
@@ -75,7 +75,7 @@ let rec rewrite_tac ~direction ~pattern:(wanted,hyps_pat,concl_pat) equality =
           [] -> assert false
         | Some (Cic.Name s,Cic.Decl ty)::_ when name = s ->
            Cic.Rel n, S.lift n ty
-        | Some (Cic.Name s,Cic.Def _)::_ -> assert false (*CSC: not implemented yet! But does this make any sense?*)
+        | Some (Cic.Name s,Cic.Def _)::_ when name = s -> assert false (*CSC: not implemented yet! But does this make any sense?*)
         | _::tl -> find_hyp (n+1) tl
       in
        let arg,gty = find_hyp 1 context in