From 672f8ee0c96584735294641bb4b8760e25197b80 Mon Sep 17 00:00:00 2001
From: Matej Kosik
Date: Mon, 14 Dec 2015 12:52:49 +0100
Subject: CLEANUP: in the Reduction module

---
 engine/evd.ml | 12 ++++++------
 1 file changed, 6 insertions(+), 6 deletions(-)

(limited to 'engine')

diff --git a/engine/evd.ml b/engine/evd.ml
index 2060141644..6651ff5f63 100644
--- a/engine/evd.ml
+++ b/engine/evd.ml
@@ -926,12 +926,12 @@ let update_sigma_env evd env =
 let test_conversion_gen env evd pb t u =
   match pb with 
   | Reduction.CONV -> 
-    Reduction.conv_universes 
-      full_transparent_state ~evars:(existential_opt_value evd) env 
-      (UState.ugraph evd.universes) t u
-  | Reduction.CUMUL -> Reduction.conv_leq_universes
-     full_transparent_state ~evars:(existential_opt_value evd) env 
-      (UState.ugraph evd.universes) t u
+    Reduction.conv env
+      ~evars:((existential_opt_value evd), (UState.ugraph evd.universes))
+      t u
+  | Reduction.CUMUL -> Reduction.conv_leq env
+      ~evars:((existential_opt_value evd), (UState.ugraph evd.universes))
+      t u
 
 let test_conversion env d pb t u =
   try test_conversion_gen env d pb t u; true
-- 
cgit v1.2.3