Fix #748 (coq.typecheck-indt-decl failing)

[proux01]

Fixes: #748

The count-prods-nored is not ideal, I would prefer using something like @redflags! coq.redflags.nored => coq.count-prods ... but this didn't worked when I tried.

[proux01]

CI green

[gares]

There are a few things that are not ok. The one that puzzles me is that if you use coq apis you must load the context correctly, but the old count prods you modified does not. Although the errors should be fatal, so I really don't know how CI did not failed.

This seems to work here

pred coq.count-prods i:term, o:int.
coq.count-prods (prod N T B) C :- !,
  (@pi-decl N T x\ coq.count-prods (B x) C'), C is C' + 1.
coq.count-prods (let N T V B) C  :- !,
  (@pi-def N T V x\ coq.count-prods (B x) C).
coq.count-prods T C :- !,
  coq.reduction.lazy.whd T Tr,
  if (T == Tr) (C = 0) (coq.count-prods Tr C).

and I tried as follows

Definition foo := nat -> nat.
Elpi command c.
Elpi Query lp:{{
(@redflags! coq.redflags.nored => coq.count-prods {{ foo }} 0),
(                                 coq.count-prods {{ foo }} 1).
}}.

Using == in place of = should not really matter much.
I removed the label, since its main objective was to let one plug in some reduction.

[gares]

I would remove the anchor point also in arity-> sort, and similarly to count prod move under let-ins without firing them (and use ==, again not foundamental).

[proux01]

@gares thanks for the review. It should now be taken into account and CI is green again.

This seems to work here

Indeed, it appears the issue I actually experienced wasn't with redflags but the missing @pi-decl you spotted.

[proux01]

Thanks