From 9ec87c4fb09876d001082d6480ba23f9f3eac361 Mon Sep 17 00:00:00 2001 From: Pierre Roux Date: Thu, 23 Jan 2025 09:23:56 +0100 Subject: [PATCH] Revert "Adapt to https://github.com/LPCIC/coq-elpi/pull/750" This reverts commit 82ee41024b535bdefff405a11188a88c729e267e. --- HB/common/utils.elpi | 7 +------ 1 file changed, 1 insertion(+), 6 deletions(-) diff --git a/HB/common/utils.elpi b/HB/common/utils.elpi index 92b11e713..ae4216b66 100644 --- a/HB/common/utils.elpi +++ b/HB/common/utils.elpi @@ -324,14 +324,9 @@ pred prod-last-gref i:term, o:gref. prod-last-gref (prod N S X) GR :- !, @pi-decl N S x\ prod-last-gref (X x) GR. prod-last-gref X GR :- coq.term->gref X GR. -pred count-prods-nored i:term, o:int. -count-prods-nored (prod _ _ B) N :- !, (pi x\ count-prods-nored (B x) M), N is M + 1. -count-prods-nored (let _ _ _ B) N :- !, (pi x\ count-prods-nored (B x) N). -count-prods-nored _ 0. - % saturate a type constructor with holes pred saturate-type-constructor i:term, o:term . saturate-type-constructor T ET :- coq.typecheck T TH ok, - count-prods-nored TH N, + coq.count-prods TH N, coq.mk-app T {coq.mk-n-holes N} ET.