From 5180ab68819f10949cd41a2458bff877b3ec3204 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Mon, 15 Feb 2016 16:45:18 +0100 Subject: Using monotonic types for conversion functions. --- pretyping/reductionops.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'pretyping/reductionops.ml') diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml index 5e21154a6..a677458da 100644 --- a/pretyping/reductionops.ml +++ b/pretyping/reductionops.ml @@ -572,7 +572,7 @@ type state = constr * constr Stack.t type contextual_reduction_function = env -> evar_map -> constr -> constr type reduction_function = contextual_reduction_function type local_reduction_function = evar_map -> constr -> constr -type e_reduction_function = env -> evar_map -> constr -> evar_map * constr +type e_reduction_function = { e_redfun : 'r. env -> 'r Sigma.t -> constr -> (constr, 'r) Sigma.sigma } type contextual_stack_reduction_function = env -> evar_map -> constr -> constr * constr list -- cgit v1.2.3