diff options
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 aedc44ac8f..2b28a7147d 100644 --- a/kernel/term_typing.ml +++ b/kernel/term_typing.ml @@ -24,10 +24,7 @@ open Typeops let constrain_type env j cst1 = function | None -> -(* To have definitions in Type polymorphic - make_polymorphic_if_arity env j.uj_type, cst1 -*) - NonPolymorphicType j.uj_type, cst1 + make_polymorphic_if_constant_for_ind env j, cst1 | Some t -> let (tj,cst2) = infer_type env t in let (_,cst3) = judge_of_cast env j DEFAULTcast tj in |