diff options
| author |  msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-04-13 14:27:03 +0000 |
|---|---|---|
| committer | msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-04-13 14:27:03 +0000 |
| commit | 4909ae24a4c346935d11b034bcb6e9d5f8641d4a (patch) | |
| tree | cc2e15319c2c830f961a5b124fdbc312276a820c /kernel/term_typing.ml | |
| parent | d98dfbcae463f8d699765e2d7004becd7714d6cf (diff) | |
- 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
Diffstat (limited to 'kernel/term_typing.ml')
| -rw-r--r-- | kernel/term_typing.ml | 5 |
1 files changed, 1 insertions, 4 deletions
diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml index 9a73abfad..63639b9a6 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 -> |