diff options
| author |  Samuel Mimram <smimram@debian.org> | 2006-04-28 14:59:16 +0000 |
|---|---|---|
| committer | Samuel Mimram <smimram@debian.org> | 2006-04-28 14:59:16 +0000 |
| commit | 3ef7797ef6fc605dfafb32523261fe1b023aeecb (patch) | |
| tree | ad89c6bb57ceee608fcba2bb3435b74e0f57919e /kernel/reduction.mli | |
| parent | 018ee3b0c2be79eb81b1f65c3f3fa142d24129c8 (diff) | |
Imported Upstream version 8.0pl3+8.1alphaupstream/8.0pl3+8.1alpha
Diffstat (limited to 'kernel/reduction.mli')
| -rw-r--r-- | kernel/reduction.mli | 19 |
1 files changed, 17 insertions, 2 deletions
diff --git a/kernel/reduction.mli b/kernel/reduction.mli index c516ea70..a68e8697 100644 --- a/kernel/reduction.mli +++ b/kernel/reduction.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: reduction.mli,v 1.56.8.1 2004/07/16 19:30:26 herbelin Exp $ i*) +(*i $Id: reduction.mli 7639 2005-12-02 10:01:15Z gregoire $ i*) (*i*) open Term @@ -29,13 +29,28 @@ 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 set_vm_conv : (conv_pb -> types conversion_function) -> unit +val vm_conv : conv_pb -> types conversion_function + +val set_default_conv : (conv_pb -> types conversion_function) -> unit +val default_conv : conv_pb -> types conversion_function +val default_conv_leq : types conversion_function + (************************************************************************) (* Builds an application node, reducing beta redexes it may produce. *) |