diff options
Diffstat (limited to 'kernel/reduction.mli')
| -rw-r--r-- | kernel/reduction.mli | 19 |
1 files changed, 11 insertions, 8 deletions
diff --git a/kernel/reduction.mli b/kernel/reduction.mli index 3b9eb315..d8658d43 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 10840 2008-04-23 21:29:34Z herbelin $ i*) +(*i $Id: reduction.mli 11897 2009-02-09 19:28:02Z barras $ i*) (*i*) open Term @@ -40,15 +40,18 @@ val conv_sort : sorts conversion_function val conv_sort_leq : sorts conversion_function val trans_conv_cmp : conv_pb -> constr trans_conversion_function - -val trans_conv : constr trans_conversion_function -val trans_conv_leq : types trans_conversion_function +val trans_conv : + ?evars:(existential->constr option) -> constr trans_conversion_function +val trans_conv_leq : + ?evars:(existential->constr option) -> types trans_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 +val conv : + ?evars:(existential->constr option) -> constr conversion_function +val conv_leq : + ?evars:(existential->constr option) -> types conversion_function +val conv_leq_vecti : + ?evars:(existential->constr option) -> types array conversion_function (* option for conversion *) val set_vm_conv : (conv_pb -> types conversion_function) -> unit |