diff options
| author | glondu | 2009-10-28 16:48:36 +0000 |
|---|---|---|
| committer | glondu | 2009-10-28 16:48:36 +0000 |
| commit | c14986c2fa8c8563f7da68d98b7c0b7f6ea2c9e7 (patch) | |
| tree | fc293a0e97ae8619ca629bccc14a48d62c02a925 | |
| parent | 7c151ae076fe5ebba9a2ea507f8f4a235feab9c7 (diff) | |
Remove old compatibility stuff (Tacred.nf)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12436 85f007b7-540e-0410-9357-904b9bb8a0f7
| -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 = |