From 0b0194b266f241b6400fecf0ff650402e4e7f0b7 Mon Sep 17 00:00:00 2001
From: puech
Date: Thu, 11 Mar 2010 15:02:41 +0000
Subject: No delta-reduction in libtypes anymore

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12858 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 toplevel/libtypes.ml | 8 +++++---
 1 file changed, 5 insertions(+), 3 deletions(-)

diff --git a/toplevel/libtypes.ml b/toplevel/libtypes.ml
index 7a065ae028..04064025f2 100644
--- a/toplevel/libtypes.ml
+++ b/toplevel/libtypes.ml
@@ -15,9 +15,11 @@ open Names
  * Module construction
  *)
 
-let reduce c = Reductionops.head_unfold_under_prod
-  (Auto.Hint_db.transparent_state (Auto.searchtable_map "typeclass_instances"))
-  (Global.env()) Evd.empty c
+(* let reduce c = Reductionops.head_unfold_under_prod *)
+(*   (Auto.Hint_db.transparent_state (Auto.searchtable_map "typeclass_instances")) *)
+(*   (Global.env()) Evd.empty c *)
+
+let reduce c = c
 
 module TypeDnet = Term_dnet.Make
   (struct
-- 
cgit v1.2.3