diff options
| -rw-r--r-- | pretyping/tacred.ml | 2 | ||||
| -rw-r--r-- | pretyping/tacred.mli | 5 | ||||
| -rw-r--r-- | proofs/tacmach.ml | 2 | ||||
| -rw-r--r-- | tactics/equality.ml | 4 |
4 files changed, 3 insertions, 10 deletions
diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml index 51c00122b5..a9732be47b 100644 --- a/pretyping/tacred.ml +++ b/pretyping/tacred.ml @@ -730,8 +730,6 @@ let whd_simpl env sigma c = let simpl env sigma c = strong whd_simpl env sigma c -let nf = simpl (* Compatibility *) - (* Reduction at specific subterms *) let is_head c t = diff --git a/pretyping/tacred.mli b/pretyping/tacred.mli index 26d62379ac..80eca2bcc5 100644 --- a/pretyping/tacred.mli +++ b/pretyping/tacred.mli @@ -94,8 +94,3 @@ val reduce_to_atomic_ref : val contextually : bool -> occurrences * constr -> reduction_function -> reduction_function - -(* Compatibility *) -(* use [simpl] instead of [nf] *) -val nf : reduction_function - diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml index 0faba52eae..754d98616f 100644 --- a/proofs/tacmach.ml +++ b/proofs/tacmach.ml @@ -98,7 +98,7 @@ let pf_whd_betadeltaiota = pf_reduce whd_betadeltaiota let pf_whd_betadeltaiota_stack = pf_reduce whd_betadeltaiota_stack let pf_hnf_constr = pf_reduce hnf_constr let pf_red_product = pf_reduce red_product -let pf_nf = pf_reduce nf +let pf_nf = pf_reduce simpl let pf_nf_betaiota = pf_reduce (fun _ -> nf_betaiota) let pf_compute = pf_reduce compute let pf_unfoldn ubinds = pf_reduce (unfoldn ubinds) diff --git a/tactics/equality.ml b/tactics/equality.ml index 200b6deb71..9957e8a393 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -919,8 +919,8 @@ let try_delta_expand env sigma t = let simplify_args env sigma t = (* Quick hack to reduce in arguments of eq only *) match decompose_app t with - | eq, [t;c1;c2] -> applist (eq,[t;nf env sigma c1;nf env sigma c2]) - | eq, [t1;c1;t2;c2] -> applist (eq,[t1;nf env sigma c1;t2;nf env sigma c2]) + | eq, [t;c1;c2] -> applist (eq,[t;simpl env sigma c1;simpl env sigma c2]) + | eq, [t1;c1;t2;c2] -> applist (eq,[t1;simpl env sigma c1;t2;simpl env sigma c2]) | _ -> t let inject_at_positions env sigma (eq,_,(t,t1,t2)) eq_clause posns tac = |