diff options
| -rw-r--r-- | tactics/tactics.ml | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 1c1843a124..71ac43c74c 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -1395,7 +1395,8 @@ let ipat_of_name = function let allow_replace c gl = function (* A rather arbitrary condition... *) | Some (_, IntroIdentifier id) -> - fst (decompose_app ((strip_lam_assum c))) = mkVar id + let c = fst (decompose_app ((strip_lam_assum c))) in + isVar c && destVar c = id | _ -> false |