diff options
Diffstat (limited to 'kernel/reduction.mli')
| -rw-r--r-- | kernel/reduction.mli | 17 |
1 files changed, 11 insertions, 6 deletions
diff --git a/kernel/reduction.mli b/kernel/reduction.mli index 0df26d6276..7db7e57bb5 100644 --- a/kernel/reduction.mli +++ b/kernel/reduction.mli @@ -28,7 +28,7 @@ exception NotConvertibleVect of int type 'a conversion_function = env -> 'a -> 'a -> unit type 'a trans_conversion_function = Names.transparent_state -> 'a conversion_function -type 'a universe_conversion_function = env -> Univ.universes -> 'a -> 'a -> unit +type 'a universe_conversion_function = env -> UGraph.t -> 'a -> 'a -> unit type 'a trans_universe_conversion_function = Names.transparent_state -> 'a universe_conversion_function @@ -45,7 +45,7 @@ type 'a universe_state = 'a * 'a universe_compare type ('a,'b) generic_conversion_function = env -> 'b universe_state -> 'a -> 'a -> 'b -type 'a infer_conversion_function = env -> Univ.universes -> 'a -> 'a -> Univ.constraints +type 'a infer_conversion_function = env -> UGraph.t -> 'a -> 'a -> Univ.constraints val sort_cmp_universes : env -> conv_pb -> sorts -> sorts -> 'a * 'a universe_compare -> 'a * 'a universe_compare @@ -55,8 +55,8 @@ constructors. *) val convert_instances : flex:bool -> Univ.Instance.t -> Univ.Instance.t -> 'a * 'a universe_compare -> 'a * 'a universe_compare -val checked_universes : Univ.universes universe_compare -val inferred_universes : (Univ.universes * Univ.Constraint.t) universe_compare +val checked_universes : UGraph.t universe_compare +val inferred_universes : (UGraph.t * Univ.Constraint.t) universe_compare val trans_conv_cmp : ?l2r:bool -> conv_pb -> constr trans_conversion_function val trans_conv : @@ -97,14 +97,19 @@ val default_conv_leq : ?l2r:bool -> types conversion_function (************************************************************************) (** Builds an application node, reducing beta redexes it may produce. *) +val beta_applist : constr -> constr list -> constr + +(** 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. *) -val betazeta_appvect : int -> constr -> constr array -> constr +(** Builds an application node, reducing beta redexe it may produce. *) +val beta_app : constr -> constr -> constr (** Pseudo-reduction rule Prod(x,A,B) a --> B[x\a] *) val hnf_prod_applist : env -> types -> constr list -> types +(** Compatibility alias for Term.lambda_appvect_assum *) +val betazeta_appvect : int -> constr -> constr array -> constr (*********************************************************************** s Recognizing products and arities modulo reduction *) |