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
---
 kernel/term_typing.ml | 5 +----
 1 file changed, 1 insertion(+), 4 deletions(-)

(limited to 'kernel')

diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml
index 9a73abfadd..63639b9a65 100644
--- a/kernel/term_typing.ml
+++ b/kernel/term_typing.ml
@@ -33,10 +33,7 @@ let constrain_type env j cst1 poly = function
       let (_,cst3) = judge_of_cast env j DEFAULTcast tj in
 	assert (t = tj.utj_val);
 	let cstrs = union_constraints (union_constraints cst1 cst2) cst3 in
-	  if poly then 
-	    make_polymorphic env { j with uj_type = tj.utj_val }, cstrs
-	  else
-	    NonPolymorphicType t, cstrs
+	  NonPolymorphicType t, cstrs
 
 let local_constrain_type env j cst1 = function
   | None ->
-- 
cgit v1.2.3