diff options
| -rw-r--r-- | pretyping/tacred.ml | 6 | ||||
| -rw-r--r-- | pretyping/tacred.mli | 3 | ||||
| -rw-r--r-- | tactics/tactics.ml | 2 |
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) |