From 47bf3b7fee031096013b29ad496949de063f010a Mon Sep 17 00:00:00 2001
From: herbelin
Date: Fri, 5 May 2000 13:29:20 +0000
Subject: Ajout d'un strong 'light'

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

(limited to 'kernel/reduction.mli')

diff --git a/kernel/reduction.mli b/kernel/reduction.mli
index 25adf3b889..c772ede665 100644
--- a/kernel/reduction.mli
+++ b/kernel/reduction.mli
@@ -16,7 +16,9 @@ open Closure
 exception Redelimination
 exception Elimconst
 
-type 'a reduction_function = env -> 'a evar_map -> constr -> constr
+type 'a contextual_reduction_function = env -> 'a evar_map -> constr -> constr
+type 'a reduction_function = 'a contextual_reduction_function
+type local_reduction_function = constr -> constr
 
 type 'a stack_reduction_function = 
     env -> 'a evar_map -> constr -> constr list -> constr * constr list
@@ -27,6 +29,7 @@ val whd_stack : 'a stack_reduction_function
 
 val under_casts : 'a reduction_function -> 'a reduction_function
 val strong : 'a reduction_function -> 'a reduction_function
+val local_strong : local_reduction_function -> local_reduction_function
 val strong_prodspine : 'a reduction_function -> 'a reduction_function
 val stack_reduction_of_reduction : 
   'a reduction_function -> 'a stack_reduction_function
-- 
cgit v1.2.3