Bug introduit avec le 'Simpl f'

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4971 85f007b7-540e-0410-9357-904b9bb8a0f7

3 files changed, 6 insertions, 5 deletions

diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml
index c26e9ce05c..41b393a322 100644
--- a/pretyping/tacred.ml
+++ b/pretyping/tacred.ml
@@ -606,7 +606,7 @@ let is_head c t =
     | App (f,_) -> f = c
     | _ -> false
 
-let contextually (locs,c) f env sigma t =
+let contextually byheadalso (locs,c) f env sigma t =
   let maxocc = List.fold_right max locs 0 in
   let pos = ref 1 in
   let check = ref true in
@@ -617,7 +617,7 @@ let contextually (locs,c) f env sigma t =
    let rec traverse (env,c as envc) t =
     if locs <> [] & (not except) & (!pos > maxocc) then t
     else
-    if eq_constr c t or is_head c t then
+    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
@@ -843,7 +843,7 @@ let declare_red_expr s f =
 let reduction_of_redexp = function
   | Red internal -> if internal then internal_red_product else red_product
   | Hnf -> hnf_constr
-  | Simpl (Some lp) -> contextually lp nf
+  | Simpl (Some lp) -> contextually true lp nf
   | Simpl None -> nf
   | Cbv f -> cbv_norm_flags (make_flag f)
   | Lazy f -> clos_norm_flags (make_flag f)
diff --git a/pretyping/tacred.mli b/pretyping/tacred.mli
index c97a27f6ad..32e40d3ac5 100644
--- a/pretyping/tacred.mli
+++ b/pretyping/tacred.mli
@@ -68,7 +68,8 @@ val reduce_to_quantified_ref :
 
 type red_expr = (constr, evaluable_global_reference) red_expr_gen
 
-val contextually : constr occurrences -> reduction_function->reduction_function
+val contextually : bool -> constr occurrences -> reduction_function
+  -> reduction_function
 val reduction_of_redexp : red_expr -> reduction_function
 
 val declare_red_expr : string -> reduction_function -> unit
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 5d2a0c6b71..4a864bbf38 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -181,7 +181,7 @@ let change_and_check cv_pb t env sigma c =
 (* Use cumulutavity only if changing the conclusion not a subterm *)
 let change_on_subterm cv_pb t = function
   | None -> change_and_check cv_pb t
-  | Some occl -> contextually occl (change_and_check CONV t) 
+  | Some occl -> contextually false occl (change_and_check CONV t) 
 
 let change_in_concl occl t = reduct_in_concl (change_on_subterm CUMUL t occl) 
 let change_in_hyp occl t   = reduct_in_hyp (change_on_subterm CONV t occl)