aboutsummaryrefslogtreecommitdiffhomepage
path: root/toplevel/libtypes.ml
diff options
context:
space:
mode:
Diffstat (limited to 'toplevel/libtypes.ml')
-rw-r--r--toplevel/libtypes.ml8
1 files changed, 5 insertions, 3 deletions
diff --git a/toplevel/libtypes.ml b/toplevel/libtypes.ml
index 7a065ae02..04064025f 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