diff options
| author |  Stephane Glondu <steph@glondu.net> | 2009-02-19 13:13:14 +0100 |
|---|---|---|
| committer | Stephane Glondu <steph@glondu.net> | 2009-02-19 13:13:14 +0100 |
| commit | a0a94c1340a63cdb824507b973393882666ba52a (patch) | |
| tree | 73aa4eb32cbd176379bc91b21c184e2a6882bfe3 /kernel/reduction.mli | |
| parent | cfbfe13f5b515ae2e3c6cdd97e2ccee03bc26e56 (diff) | |
Imported Upstream version 8.2-1+dfsgupstream/8.2-1+dfsg
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 |