From 3ef7797ef6fc605dfafb32523261fe1b023aeecb Mon Sep 17 00:00:00 2001 From: Samuel Mimram Date: Fri, 28 Apr 2006 14:59:16 +0000 Subject: Imported Upstream version 8.0pl3+8.1alpha --- kernel/reduction.mli | 19 +++++++++++++++++-- 1 file changed, 17 insertions(+), 2 deletions(-) (limited to 'kernel/reduction.mli') 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. *) -- cgit v1.2.3