From 61ccbc81a2f3b4662ed4a2bad9d07d2003dda3a2 Mon Sep 17 00:00:00 2001 From: glondu Date: Thu, 17 Sep 2009 15:58:14 +0000 Subject: Delete trailing whitespaces in all *.{v,ml*} files git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12337 85f007b7-540e-0410-9357-904b9bb8a0f7 --- kernel/reduction.mli | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) (limited to 'kernel/reduction.mli') diff --git a/kernel/reduction.mli b/kernel/reduction.mli index 9960513294..f2c9df1568 100644 --- a/kernel/reduction.mli +++ b/kernel/reduction.mli @@ -33,7 +33,7 @@ type 'a trans_conversion_function = Names.transparent_state -> env -> 'a -> 'a - type conv_pb = CONV | CUMUL -val sort_cmp : +val sort_cmp : conv_pb -> sorts -> sorts -> Univ.constraints -> Univ.constraints val conv_sort : sorts conversion_function @@ -63,10 +63,10 @@ val default_conv_leq : types conversion_function (************************************************************************) -(* Builds an application node, reducing beta redexes it may produce. *) +(* Builds an application node, reducing beta redexes it may produce. *) val beta_appvect : constr -> constr array -> constr -(* Builds an application node, reducing the [n] first beta-zeta redexes. *) +(* Builds an application node, reducing the [n] first beta-zeta redexes. *) val betazeta_appvect : int -> constr -> constr array -> constr (* Pseudo-reduction rule Prod(x,A,B) a --> B[x\a] *) -- cgit v1.2.3