From 14b6df0f5a23a231ade989bb1e3dab0f657d1fab Mon Sep 17 00:00:00 2001
From: ppedrot
Date: Tue, 22 Oct 2013 17:26:22 +0000
Subject: Various optimizations in Constr, such as term sharing and allocation
 avoiding.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16911 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 pretyping/reductionops.ml | 14 ++++++++++----
 1 file changed, 10 insertions(+), 4 deletions(-)

(limited to 'pretyping')

diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index 3860cc015c..dbb78e9c36 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -647,8 +647,9 @@ let nf_evar =
    a [nf_evar] here *)
 let clos_norm_flags flgs env sigma t =
   try
+    let evars ev = safe_evar_value sigma ev in
     norm_val
-      (create_clos_infos ~evars:(safe_evar_value sigma) flgs env)
+      (create_clos_infos ~evars flgs env)
       (inject t)
   with e when is_anomaly e -> error "Tried to normalize ill-typed term"
 
@@ -752,8 +753,10 @@ let pb_equal = function
 let sort_cmp = sort_cmp
 
 let test_conversion (f: ?l2r:bool-> ?evars:'a->'b) env sigma x y =
-  try let _ =
-    f ~evars:(safe_evar_value sigma) env x y in true
+  try
+    let evars ev = safe_evar_value sigma ev in
+    let _ = f ~evars env x y in
+    true
   with NotConvertible -> false
     | e when is_anomaly e -> error "Conversion test raised an anomaly"
 
@@ -762,7 +765,10 @@ let is_conv_leq env sigma = test_conversion Reduction.conv_leq env sigma
 let is_fconv = function | CONV -> is_conv | CUMUL -> is_conv_leq
 
 let test_trans_conversion (f: ?l2r:bool-> ?evars:'a->'b) reds env sigma x y =
-  try let _ = f ~evars:(safe_evar_value sigma) reds env x y in true
+  try
+    let evars ev = safe_evar_value sigma ev in
+    let _ = f ~evars reds env x y in
+    true
   with NotConvertible -> false
     | e when is_anomaly e -> error "Conversion test raised an anomaly"
 
-- 
cgit v1.2.3