+let proc_gref ss = function
+ | C.Constant _ , R.Decl ->
+ T.Macro "GRef" :: T.mk_segs ("type" :: ss)
+ | C.Constant _ , R.Def _ ->
+ T.Macro "GRef" :: T.mk_segs ("body" :: ss)
+ | C.Inductive (_, _, us, _), R.Ind (_, i, _) ->
+ let _, name, _, _ = L.nth us i in
+ T.Macro "IRef" :: T.mk_segs (name :: ss)
+ | C.Inductive (_, _, us, _), R.Con (i, j, _) ->
+ let _, _, _, ts = L.nth us i in
+ let _, name, _ = L.nth ts (pred j) in
+ T.Macro "IRef" :: T.mk_segs (name :: ss)
+ | C.Fixpoint (_, ts, _) , R.Fix (i, _, _) ->
+ let _, name, _, _, _ = L.nth ts i in
+ T.Macro "IRef" :: T.mk_segs (name :: ss)
+ | C.Fixpoint (_, ts, _) , R.CoFix i ->
+ let _, name, _, _, _ = L.nth ts i in
+ T.Macro "IRef" :: T.mk_segs (name :: ss)
+ | _ ->
+ malformed "2"