From f3f62cf19a67d62f985909728ac859521e554831 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Sat, 4 Dec 2004 10:52:00 +0000
Subject: Bug 'set n in * |-'

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6398 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 tactics/tactics.ml | 10 +++++-----
 1 file 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 
-- 
cgit v1.2.3