From 6160f53e89800a785d773c4130b08fbe7c345651 Mon Sep 17 00:00:00 2001
From: barras
Date: Fri, 6 Feb 2009 21:25:52 +0000
Subject: pushed evar reduction in kernel

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11889 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 kernel/reduction.mli | 17 ++++++++++-------
 1 file changed, 10 insertions(+), 7 deletions(-)

(limited to 'kernel/reduction.mli')

diff --git a/kernel/reduction.mli b/kernel/reduction.mli
index 6ac1591bbd..de926bd1d6 100644
--- a/kernel/reduction.mli
+++ b/kernel/reduction.mli
@@ -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
-- 
cgit v1.2.3