From 4909ae24a4c346935d11b034bcb6e9d5f8641d4a Mon Sep 17 00:00:00 2001
From: msozeau
Date: Wed, 13 Apr 2011 14:27:03 +0000
Subject: - Do not make constants with an assigned type polymorphic (wrong
 unfoldings). - Add Set Typeclasses Debug/Depth n options for typeclasses
 eauto.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13989 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 pretyping/typeclasses.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'pretyping')

diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml
index eabef36417..c8a99a315a 100644
--- a/pretyping/typeclasses.ml
+++ b/pretyping/typeclasses.ml
@@ -118,7 +118,7 @@ let dest_class_app env c =
     global_class_of_constr env cl, args
 
 let dest_class_arity env c =
-  let rels, c = decompose_prod_assum c in
+  let rels, c = Term.decompose_prod_assum c in
     rels, dest_class_app env c
 
 let class_of_constr c = try Some (dest_class_arity (Global.env ()) c) with _ -> None
-- 
cgit v1.2.3