From 023c516a2c0178f8e06b8ee795779fdd34aeba83 Mon Sep 17 00:00:00 2001
From: ppedrot
Date: Sun, 27 Oct 2013 15:02:36 +0000
Subject: Closure optimizations.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16937 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 pretyping/evd.ml     | 2 +-
 pretyping/termops.ml | 4 ++--
 2 files changed, 3 insertions(+), 3 deletions(-)

diff --git a/pretyping/evd.ml b/pretyping/evd.ml
index 1cc9df024b..4a188da001 100644
--- a/pretyping/evd.ml
+++ b/pretyping/evd.ml
@@ -457,7 +457,7 @@ let extract_conv_pbs evd p =
   pbs
 
 let extract_changed_conv_pbs evd p =
-  extract_conv_pbs evd (p evd.last_mods)
+  extract_conv_pbs evd (fun pb -> p evd.last_mods pb)
 
 let extract_all_conv_pbs evd =
   extract_conv_pbs evd (fun _ -> true)
diff --git a/pretyping/termops.ml b/pretyping/termops.ml
index 5fb74dcad4..6510655b99 100644
--- a/pretyping/termops.ml
+++ b/pretyping/termops.ml
@@ -895,11 +895,11 @@ let compare_constr_univ f cv_pb t1 t2 =
       Sort s1, Sort s2 -> base_sort_cmp cv_pb s1 s2
     | Prod (_,t1,c1), Prod (_,t2,c2) ->
 	f Reduction.CONV t1 t2 && f cv_pb c1 c2
-    | _ -> compare_constr (f Reduction.CONV) t1 t2
+    | _ -> compare_constr (fun t1 t2 -> f Reduction.CONV t1 t2) t1 t2
 
 let rec constr_cmp cv_pb t1 t2 = compare_constr_univ constr_cmp cv_pb t1 t2
 
-let eq_constr = constr_cmp Reduction.CONV
+let eq_constr t1 t2 = constr_cmp Reduction.CONV t1 t2
 
 (* App(c,[t1,...tn]) -> ([c,t1,...,tn-1],tn)
    App(c,[||]) -> ([],c) *)
-- 
cgit v1.2.3