diff options
| -rw-r--r-- | pretyping/evarconv.ml | 2 | ||||
| -rw-r--r-- | test-suite/bugs/closed/5368.v | 6 |
2 files changed, 8 insertions, 0 deletions
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index cb8844623..f7a3789a2 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -218,6 +218,8 @@ let check_conv_record env sigma (t1,sk1) (t2,sk2) = let t' = EConstr.of_constr t' in let t' = subst_univs_level_constr subst t' in let bs' = List.map (EConstr.of_constr %> subst_univs_level_constr subst) bs in + let params = List.map (fun c -> subst_univs_level_constr subst c) params in + let us = List.map (fun c -> subst_univs_level_constr subst c) us in let h, _ = decompose_app_vect sigma t' in ctx',(h, t2),c',bs',(Stack.append_app_list params Stack.empty,params1), (Stack.append_app_list us Stack.empty,us2),(extra_args1,extra_args2),c1, diff --git a/test-suite/bugs/closed/5368.v b/test-suite/bugs/closed/5368.v new file mode 100644 index 000000000..410fe1707 --- /dev/null +++ b/test-suite/bugs/closed/5368.v @@ -0,0 +1,6 @@ +Set Universe Polymorphism. + +Record cantype := {T:Type; op:T -> unit}. +Canonical Structure test (P:Type) := {| T := P -> Type; op := fun _ => tt|}. + +Check (op _ ((fun (_:unit) => Set):_)). |