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

1 files changed, 13 insertions, 4 deletions

diff --git a/pretyping/tacred.mli b/pretyping/tacred.mli
index 84cc87e7f0..0ff5154f60 100644
--- a/pretyping/tacred.mli
+++ b/pretyping/tacred.mli
@@ -35,11 +35,15 @@ val red_product : reduction_function
 (* Red (raise Redelimination if nothing reducible) *)
 val try_red_product : reduction_function
 
-(* Hnf *)
-val hnf_constr :  reduction_function
-
 (* Simpl *)
-val nf :  reduction_function
+val simpl : reduction_function 
+
+(* Simpl only at the head *)
+val whd_simpl : reduction_function
+
+(* Hnf: like whd_simpl but force delta-reduction of constants that do
+   not immediately hide a non reducible fix or cofix *)
+val hnf_constr : reduction_function
 
 (* Unfold *)
 val unfoldn : 
@@ -79,3 +83,8 @@ val reduce_to_atomic_ref :
 
 val contextually : bool -> int list * constr -> reduction_function
   -> reduction_function
+
+(* Compatibility *)
+(* use [simpl] instead of [nf] *)
+val nf :  reduction_function
+