From e7d592ada2d681876d2bcf0a45d4267b3746064f Mon Sep 17 00:00:00 2001
From: herbelin
Date: Wed, 14 Feb 2001 15:41:55 +0000
Subject: Mise en place d'un système optionnel de discharge immédiat; prise en
 compte des défs locales dans les arguments des inductifs; nettoyage divers

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1381 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 kernel/reduction.mli | 3 +++
 1 file changed, 3 insertions(+)

(limited to 'kernel/reduction.mli')

diff --git a/kernel/reduction.mli b/kernel/reduction.mli
index 600cdd8230..794c493544 100644
--- a/kernel/reduction.mli
+++ b/kernel/reduction.mli
@@ -59,16 +59,19 @@ val nf_betadeltaiota : 'a reduction_function
 val whd_beta : local_reduction_function
 val whd_betaiota : local_reduction_function
 val whd_betadeltaiota : 'a contextual_reduction_function
+val whd_betadeltaiota_nolet : 'a contextual_reduction_function
 val whd_betaetalet : local_reduction_function
 
 val whd_beta_stack : local_stack_reduction_function
 val whd_betaiota_stack : local_stack_reduction_function
 val whd_betadeltaiota_stack : 'a contextual_stack_reduction_function
+val whd_betadeltaiota_nolet_stack : 'a contextual_stack_reduction_function
 val whd_betaetalet_stack : local_stack_reduction_function
 
 val whd_beta_state : local_state_reduction_function
 val whd_betaiota_state : local_state_reduction_function
 val whd_betadeltaiota_state : 'a contextual_state_reduction_function
+val whd_betadeltaiota_nolet_state : 'a contextual_state_reduction_function
 val whd_betaetalet_state : local_state_reduction_function
 
 (*s Head normal forms *)
-- 
cgit v1.2.3