diff options
| -rw-r--r-- | tactics/tactics.ml | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 314bcd55f8..872baa1799 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -651,7 +651,7 @@ let occurrences_of_hyp id cls = let occurrences_of_goal cls = if cls.onconcl then Some cls.concl_occs else None -let everywhere cls = (cls=allClauses) +let in_every_hyp cls = (cls.onhyps=None) (* (* Implementation with generalisation then re-intro: introduces noise *) @@ -666,8 +666,8 @@ let letin_abstract id c occs gl = | None -> raise Not_found | Some occ -> let newdecl = subst_term_occ_decl occ c d in - if d = newdecl then - if not (everywhere occs) + if occ = [] & d = newdecl then + if not (in_every_hyp occs) then raise (RefinerError (DoesNotOccurIn (c,hyp))) else raise Not_found else @@ -718,8 +718,8 @@ let letin_abstract id c occs gl = | None -> depdecls | Some occ -> let newdecl = subst_term_occ_decl occ c d in - if d = newdecl then - if not (everywhere occs) + if occ = [] & d = newdecl then + if not (in_every_hyp occs) then raise (RefinerError (DoesNotOccurIn (c,hyp))) else depdecls else |