diff options
| author |  barras <barras@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2004-10-20 13:50:08 +0000 |
|---|---|---|
| committer | barras <barras@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2004-10-20 13:50:08 +0000 |
| commit | 9c6487ba87f448daa28158c6e916e3d932c50645 (patch) | |
| tree | 31bc965d5d14b34d4ab501cbd2350d1de44750c5 /kernel/reduction.mli | |
| parent | 1457d6a431755627e3b52eaf74ddd09c641a9fe3 (diff) | |
COMMITED BYTECODE COMPILER
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6245 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'kernel/reduction.mli')
| -rw-r--r-- | kernel/reduction.mli | 15 |
1 files changed, 14 insertions, 1 deletions
diff --git a/kernel/reduction.mli b/kernel/reduction.mli index 4f519fff7..ca4ab8c94 100644 --- a/kernel/reduction.mli +++ b/kernel/reduction.mli @@ -29,13 +29,26 @@ exception NotConvertible exception NotConvertibleVect of int type 'a conversion_function = env -> 'a -> 'a -> Univ.constraints +type conv_pb = CONV | CUMUL + +val sort_cmp : + conv_pb -> sorts -> sorts -> Univ.constraints -> Univ.constraints + val conv_sort : sorts conversion_function val conv_sort_leq : sorts conversion_function -val conv : types conversion_function +val conv_cmp : conv_pb -> constr conversion_function + +val conv : constr conversion_function val conv_leq : types conversion_function val conv_leq_vecti : types array conversion_function +(* option for conversion *) +val use_vm : bool ref +val set_vm_conv_cmp : (conv_pb -> types conversion_function) -> unit +val vm_conv : conv_pb -> types conversion_function +val vm_conv_leq_vecti : types array conversion_function + (************************************************************************) (* Builds an application node, reducing beta redexes it may produce. *) |