Nettoyage des tactiques basées sur "simpl" (delta-réduction cachant

fix/cofix avec réutilisation du nom de la constante dans les appels
récursifs), avec notamment uniformisation des comportements et des
noms de fonctions de réduction. En particulier, on a les changements
sémantiques suivants :

- léger changement de simpl: si appliqué à un fix explicite, il sait
  réduire l'argument en un constructeur comme si le fix était caché
  derrière une constante (cf exemple dans test-suite/output/reduction.v);
- léger changement de hnf: si appliqué à un match ou un fix explicite
  et que l'argument de ce match ou de ce fix nécessite un calcul
  impliquant des constantes récursives, il sait conserver les noms (à
  la manière de simpl) comme il sait déjà le faire si ce match ou ce fix
  était caché derrière une constante (cf exemple dans
  test-suite/output/reduction.v);
- changement similaire de one_step_reduce utilisé dans reduce_to_*_ref
  (difficile d'imaginer les effets mais sans doute très peu)



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

2 files changed, 4 insertions, 4 deletions

diff --git a/tactics/setoid_replace.ml b/tactics/setoid_replace.ml
index 500a7f40d..1273c65e4 100644
--- a/tactics/setoid_replace.ml
+++ b/tactics/setoid_replace.ml
@@ -903,7 +903,7 @@ let new_morphism m signature id hook =
       (Closure.unfold_red(Lazy.force coq_make_compatibility_goal_aux_eval_ref))
       env Evd.empty lem in
     (* "simpl" *)
-  let lem = Tacred.nf env Evd.empty lem in
+  let lem = Tacred.simpl env Evd.empty lem in
     if Lib.is_modtype () then
       begin
 	ignore
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 9e25055e9..f9e623469 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -208,9 +208,9 @@ let red_option          = reduct_option   (red_product,DEFAULTcast)
 let hnf_in_concl        = reduct_in_concl (hnf_constr,DEFAULTcast)
 let hnf_in_hyp          = reduct_in_hyp   hnf_constr
 let hnf_option          = reduct_option   (hnf_constr,DEFAULTcast)
-let simpl_in_concl      = reduct_in_concl (nf,DEFAULTcast)
-let simpl_in_hyp        = reduct_in_hyp   nf
-let simpl_option        = reduct_option   (nf,DEFAULTcast)
+let simpl_in_concl      = reduct_in_concl (simpl,DEFAULTcast)
+let simpl_in_hyp        = reduct_in_hyp   simpl
+let simpl_option        = reduct_option   (simpl,DEFAULTcast)
 let normalise_in_concl  = reduct_in_concl (compute,DEFAULTcast)
 let normalise_in_hyp    = reduct_in_hyp   compute
 let normalise_option    = reduct_option   (compute,DEFAULTcast)