Duplicate code getting parametricity classes

[ecranceMERCE]

There seems to be a duplicate implementation of a predicate that gets all parametricity classes (i.e., annotations on universes, variable or ground) present in a type.

trocq/elpi/param-class.elpi

Lines 320 to 351 in 95f083a

	% find classes present in a term
	pred type->class i:term, o:list param-class, o:list term.
	type->class X [Class] Ts :-
	coq.safe-dest-app X HD Ts,
	(do-not-fail => coq.term->gref HD GRClass),
	trocq.db.gref->class GRClass Class.
	type->class X [] Ts :- coq.safe-dest-app X _ Ts.
	type->class _ [] [].
	pred type->classes.rec i:term, o:list param-class, o:list param-class.
	type->classes.rec (prod N A B) OutList BLast:- !,
	@pi-decl N A x\
	type->classes.rec A AList ALast, !,
	type->classes.rec (B x) BList BLast, !,
	std.append {std.append AList ALast} BList OutList.
	type->classes.rec X [] Class :- !, type->class X Class _.
	pred type->classes.main i:term, o:list param-class, o:list param-class, o:gref, o:gref.
	type->classes.main (prod N A B) OutList BLast GR GR' :- !,
	@pi-decl N A x\
	type->classes.rec A AList ALast, !,
	type->classes.main (B x) BList BLast GR GR', !,
	std.append {std.append AList ALast} BList OutList.
	type->classes.main X [] Class GR GR' :- !,
	type->class X Class Ts, !,
	std.rev Ts [T', T | _],
	coq.term->gref T GR, coq.term->gref T' GR'.
	pred type->classes i:term, o:param-class, o:list param-class, o:gref, o:gref.
	type->classes T OutClass DepClasses GR GR' :-
	type->classes.main T DepClasses LastClass GR GR',
	if (LastClass = [OutClass]) true (OutClass = pc map0 map0).

trocq/elpi/annot.elpi

Lines 97 to 131 in 95f083a

	% get all the annotations in a type T, as well as the "output class", i.e., the parametricity class
	% of the output type of T, as an option basically returning some (A,B) for an output type PType A B,
	% and none for output types that are not sorts, because it means values of type T are not type
	% constructors, so their translation will be made at class (0,0)
	pred classes i:term, o:list param-class, o:option param-class.
	classes T Cs' Out :-
	all-classes T Cs,
	out-class T Out,
	if (not (Cs = []), Out = some C, std.last Cs LastC, LastC == C) (
	std.drop-last 1 Cs Cs'
	) (
	Cs' = Cs
	).
	pred all-classes i:term, o:list param-class.
	all-classes (app [pglobal (const PType) _, M, N]) [C] :- trocq.db.ptype PType, !,
	cstr.univ-link C M N.
	all-classes X Cs :- (X = prod _ T F ; X = fun _ T F), !,
	pi x\ std.append {all-classes T} {all-classes (F x)} Cs.
	all-classes (app L) Cs :- !,
	std.flatten {std.map L all-classes} Cs.
	all-classes X [] :- (name X ; X = global _ ; X = pglobal _ _), !.
	all-classes X _ :- coq.error "all-classes:" X.
	% output class of a term
	pred out-class i:term, o:option param-class.
	out-class (app [pglobal (const PType) _, M, N]) (some C) :- trocq.db.ptype PType, !,
	cstr.univ-link C M N.
	out-class (prod _ _ F) Out :- !, pi x\ out-class (F x) Out.
	out-class (fun _ _ _) none :- !.
	out-class (app [F|Xs]) Out :- !,
	coq.subst-fun Xs F App,
	if (App = app [F|Xs]) (Out = none) (out-class App Out).
	out-class X none :- (name X ; X = global _ ; X = pglobal _ _), !.
	out-class X _ :- coq.error "out-class:" X.

It would be nice to check whether there is an important difference between them, and document it, or drop one of them.