From 94d968e90fe06f920e6326c46c89ea06249c1522 Mon Sep 17 00:00:00 2001 From: Pierre Roux Date: Tue, 21 Jan 2025 15:55:35 +0100 Subject: [PATCH] Add some missing universe constraints --- apps/derive/elpi/param2.elpi | 2 ++ apps/derive/tests/test_param2.v | 7 +++++++ 2 files changed, 9 insertions(+) diff --git a/apps/derive/elpi/param2.elpi b/apps/derive/elpi/param2.elpi index 954aecc14..3a1ae4221 100644 --- a/apps/derive/elpi/param2.elpi +++ b/apps/derive/elpi/param2.elpi @@ -159,6 +159,8 @@ dispatch (const GR as C) Suffix Clauses :- do! [ param Ty _ TyR, coq.mk-app TyR [Term, Term] TyRTermTerm, + % coq.typecheck is needed to add universe constraints + std.assert-ok! (coq.typecheck TyRTermTerm _) "param2: illtyped param type", param X _ XR, % apparently calling the type checker with the expected type is weaker in this case std.assert-ok! (coq.typecheck XR XRTy) "param2: illtyped constant", diff --git a/apps/derive/tests/test_param2.v b/apps/derive/tests/test_param2.v index f9eff0fc7..8e6924f61 100644 --- a/apps/derive/tests/test_param2.v +++ b/apps/derive/tests/test_param2.v @@ -85,3 +85,10 @@ Elpi derive.param2 bla. Fixpoint silly (n : nat) := n. Elpi derive.param2 silly. +Definition size_of (A : Type) := A -> nat. + +Definition size_seq (A : Type) : size_of (list A) := fun _ => 0. + +Elpi derive.param2 size_of. + +Elpi derive.param2 size_seq. (* Fixed by https://github.com/LPCIC/coq-elpi/pull/754 *)