aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/output/reduction.out
diff options
context:
space:
mode:
authorGravatar herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>2007-04-13 11:50:02 +0000
committerGravatar herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>2007-04-13 11:50:02 +0000
commit556751099326b259b5f16a693af09c7642a03d82 (patch)
treecc96bde56971a48ebbf8cc650ba3a9203c3f03ac /test-suite/output/reduction.out
parenta914fb843800aefcc3833d93b0c1f260ab152d30 (diff)
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
Diffstat (limited to 'test-suite/output/reduction.out')
-rw-r--r--test-suite/output/reduction.out4
1 files changed, 4 insertions, 0 deletions
diff --git a/test-suite/output/reduction.out b/test-suite/output/reduction.out
new file mode 100644
index 000000000..ff327aa5f
--- /dev/null
+++ b/test-suite/output/reduction.out
@@ -0,0 +1,4 @@
+ = a
+ : nat
+ = n + 0
+ : nat