hack for coq.term->gref

Author: gares

HB/common/stdpp.elpi

@@ -260,6 +260,16 @@ term->cs-pattern (sort U) (cs-sort U).
 term->cs-pattern T (cs-gref GR) :- coq.term->gref T GR.
 term->cs-pattern T _ :- coq.error T "HB database: is not a valid canonical key".
 
+%hack/missing API
+:before "stop:begin"
+coq.term->gref (app [primitive (proj N J),T|_]) GR :- !, std.do! [
+  coq.typecheck T Ty ok,
+  coq.term->gref Ty (indt I),
+  coq.env.projections I Ps,
+  coq.env.primitive-projections I PPs,
+  std.map2-filter Ps PPs (x\y\gr\sigma c\x = some c, y = some (pr N J), gr = const c) [GR],
+].
+
 pred cs-pattern->name i:cs-pattern, o:string.
 cs-pattern->name cs-prod "prod".
 cs-pattern->name (cs-sort _) "sort".