diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2000-05-05 13:29:20 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2000-05-05 13:29:20 +0000 |
| commit | 47bf3b7fee031096013b29ad496949de063f010a (patch) | |
| tree | e81a6604979d02840c7e6250d2da46a61dd58739 /kernel/reduction.mli | |
| parent | 40be348f4502976adc0a7612e9dcf489cfd19330 (diff) | |
Ajout d'un strong 'light'
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@426 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'kernel/reduction.mli')
| -rw-r--r-- | kernel/reduction.mli | 5 |
1 files changed, 4 insertions, 1 deletions
diff --git a/kernel/reduction.mli b/kernel/reduction.mli index 25adf3b88..c772ede66 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 |