From 9717164df828f0bcc5e07118ebc93c06b5c74f40 Mon Sep 17 00:00:00 2001 From: Pierre Roux Date: Tue, 28 Jan 2025 14:43:38 +0100 Subject: [PATCH] Add some missing universe constraints --- apps/derive/elpi/param1.elpi | 2 ++ 1 file changed, 2 insertions(+) diff --git a/apps/derive/elpi/param1.elpi b/apps/derive/elpi/param1.elpi index 045b09dea..5eca035ab 100644 --- a/apps/derive/elpi/param1.elpi +++ b/apps/derive/elpi/param1.elpi @@ -136,6 +136,8 @@ dispatch (const GR) Prefix Clauses :- !, do! [ reali V VR, reali Ty TyR, coq.mk-app TyR [Term] TyRV, + % coq.typecheck is needed to add universe constraints + std.assert-ok! (coq.typecheck TyRV _) "param1: illtyped param type", % apparently calling the type checker with the expected type is weaker in this case std.assert-ok! (coq.typecheck VR VRTy) "param1: illtyped constant", std.assert-ok! (coq.unify-leq VRTy TyRV) "param1: constant does not have the right type",