From 4b7b2590e1e35a425e6d82bf280189d2ff9d27e4 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Wed, 17 Dec 2003 11:09:20 +0000
Subject: Prise en compte des sous-termes imbriqués pour 'simpl ident at nums'

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5109 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 pretyping/tacred.ml | 17 +++++++++++------
 1 file changed, 11 insertions(+), 6 deletions(-)

diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml
index 41b393a322..684dec0d36 100644
--- a/pretyping/tacred.ml
+++ b/pretyping/tacred.ml
@@ -618,12 +618,17 @@ let contextually byheadalso (locs,c) f env sigma t =
     if locs <> [] & (not except) & (!pos > maxocc) then t
     else
     if eq_constr c t or (byheadalso & is_head c t) then
-      let r =
-	if except then 
-	  if List.mem (- !pos) locs then t else f env sigma t
-	else 
-	  if locs = [] or List.mem !pos locs then f env sigma t else t
-      in incr pos; r
+      let ok = 
+	if except then not (List.mem (- !pos) locs)
+	else (locs = [] or List.mem !pos locs) in
+      incr pos;
+      if ok then
+	f env sigma t
+      else if byheadalso then
+	(* find other occurrences of c in t; TODO: ensure left-to-right *)
+	map_constr (traverse envc) t
+      else
+	t
     else
       map_constr_with_binders_left_to_right
 	(fun d (env,c) -> (push_rel d env,lift 1 c))
-- 
cgit v1.2.3