From 5af5bff88fa49731acbf24d8a67148e4215446bd Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Sun, 22 Apr 2018 16:51:25 +0200 Subject: Fix #7327: coqchk subtyping of polymorphic constants --- checker/subtyping.ml | 13 ++++++++++++- 1 file changed, 12 insertions(+), 1 deletion(-) (limited to 'checker/subtyping.ml') diff --git a/checker/subtyping.ml b/checker/subtyping.ml index 5cb38cb81..5c672d04a 100644 --- a/checker/subtyping.ml +++ b/checker/subtyping.ml @@ -303,7 +303,18 @@ let check_constant env mp1 l info1 cb2 spec2 subst1 subst2 = | Constant cb1 -> let cb1 = subst_const_body subst1 cb1 in let cb2 = subst_const_body subst2 cb2 in - (*Start by checking types*) + (*Start by checking universes *) + let env = + match cb1.const_universes, cb2.const_universes with + | Monomorphic_const _, Monomorphic_const _ -> env + | Polymorphic_const auctx1, Polymorphic_const auctx2 -> + check_polymorphic_instance error env auctx1 auctx2 + | Monomorphic_const _, Polymorphic_const _ -> + error () + | Polymorphic_const _, Monomorphic_const _ -> + error () + in + (* Now check types *) let typ1 = cb1.const_type in let typ2 = cb2.const_type in check_type env typ1 typ2; -- cgit v1.2.3