From 0980dbb1740c8d48d8ff0c516929f27f8cea854d Mon Sep 17 00:00:00 2001
From: Matej Košík
Date: Mon, 10 Apr 2017 16:04:28 +0200
Subject: Revert "refactoring: Reductionops.contextual_reduction_function type"

This reverts commit 470d0d56467a3a587dc34f958ffea8259618d1ae.
---
 pretyping/reductionops.mli | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli
index 2a5f97f010..4cd7a2a869 100644
--- a/pretyping/reductionops.mli
+++ b/pretyping/reductionops.mli
@@ -109,9 +109,9 @@ end
 
 type state = constr * constr Stack.t
 
-type local_reduction_function = evar_map -> constr -> constr
-type contextual_reduction_function = env -> local_reduction_function
+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 = { e_redfun : 'r. env -> 'r Sigma.t -> constr -> (constr, 'r) Sigma.sigma }
 
-- 
cgit v1.2.3