From 556751099326b259b5f16a693af09c7642a03d82 Mon Sep 17 00:00:00 2001 From: herbelin Date: Fri, 13 Apr 2007 11:50:02 +0000 Subject: 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 : MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit - 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 --- proofs/redexpr.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'proofs') diff --git a/proofs/redexpr.ml b/proofs/redexpr.ml index c69d1be36..2f85b18e5 100644 --- a/proofs/redexpr.ml +++ b/proofs/redexpr.ml @@ -106,8 +106,8 @@ let reduction_of_red_expr = function else (red_product,DEFAULTcast) | Hnf -> (hnf_constr,DEFAULTcast) | Simpl (Some (_,c as lp)) -> - (contextually (is_reference c) (out_with_occurrences lp) nf,DEFAULTcast) - | Simpl None -> (nf,DEFAULTcast) + (contextually (is_reference c) (out_with_occurrences lp) simpl,DEFAULTcast) + | Simpl None -> (simpl,DEFAULTcast) | Cbv f -> (cbv_norm_flags (make_flag f),DEFAULTcast) | Lazy f -> (clos_norm_flags (make_flag f),DEFAULTcast) | Unfold ubinds -> (unfoldn (List.map out_with_occurrences ubinds),DEFAULTcast) -- cgit v1.2.3