Support grefclass

[proux01]

I need this when porting all the closedness predicates in ssralg.v in mathcomp, in order to have their sort of type {pred _} rather than _ -> bool and write _ \in S rather than _ \in (S : pred _) everywhere.

[gares]

Suggested change

	build-type-pattern GR Pat :- coq.env.typeof GR T,
	build-type-pattern GR Pat :-

[gares]

I think I'd like a comment for what this piece of code is supposed to do.
Isn't it something like

coq.safe-dest-app Ty (global GR) Args,
coq.subst-prod T Args {{ Type }}

?

[proux01]

Indeed, comment added. The main idea is as follows:

• in case sortclass, we know the sort is of some type Type, so we unify with Type
• in case funclass, we know the sort is a function, so we unify with _ -> _
• in case grefclass GR, we know the sort is of type GR x1 ... xn when GR : forall x1 ... xn, Type, so we unify with GR _ ... _ (with n holes)

[gares]

I let @CohenCyril look at the phant thingy, since It is too hard for me.
The rest seems ok.

[CohenCyril]

Nice!