diff options
| author | herbelin | 2004-12-04 10:52:00 +0000 |
|---|---|---|
| committer | herbelin | 2004-12-04 10:52:00 +0000 |
| commit | f3f62cf19a67d62f985909728ac859521e554831 (patch) | |
| tree | b059eeea6ffe416f56e10187fe9bd5429f9ff9f8 | |
| parent | b1cf3efa7e75fc525590789208c8be8130074fe5 (diff) | |
Bug 'set n in * |-'
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6398 85f007b7-540e-0410-9357-904b9bb8a0f7
| -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 |