diff options
Diffstat (limited to 'kernel/term_typing.ml')
| -rw-r--r-- | kernel/term_typing.ml | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml index d834504ab..8b0f45ac9 100644 --- a/kernel/term_typing.ml +++ b/kernel/term_typing.ml @@ -24,7 +24,10 @@ 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 | Some t -> let (tj,cst2) = infer_type env t in let (_,cst3) = judge_of_cast env j DEFAULTcast tj in |