Merge pull request #759 from proux01/param1-add-typecheck

[derive.param1] Add some missing universe constraints
LPCIC · Jan 28, 2025 · 5484806 · 5484806
2 parents fd11b7a + 9717164
commit 5484806
Showing 1 changed file with 2 additions and 0 deletions.
diff --git 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",