- | RURule _ _ _ _ r => nd_urule2latex r
- | RNote x n z => "Note"
- | RLit Γ _ l _ => "Lit"
- | RVar Γ _ σ p => "Var"
- | RLam Γ _ Σ tx te p x => "Abs"
- | RCast Γ _ Σ σ τ γ p x => "Cast"
- | RAbsT Γ Σ κ σ a p => "AbsT"
- | RAppT Γ _ Σ κ σ τ p y => "AppT"
- | RAppCo Γ _ Σ κ _ σ₁ σ₂ σ γ p => "AppCo"
- | RAbsCo Γ Σ κ σ cc σ₁ σ₂ p y q => "AbsCo"
- | RApp Γ _ Σ₁ Σ₂ tx te p => "App"
- | RLet Γ _ Σ₁ Σ₂ σ₁ σ₂ p => "Let"
- | REmptyGroup _ a => "REmptyGroup"
- | RBindingGroup _ a b c d e => "RBindingGroup"
- | RLetRec Γ _ p lri q => "LetRec"
- | RCase Σ Γ T κlen κ ldcd τ _ _ => "Case"
- | RBrak Σ _ a b c _ => "Brak"
- | REsc Σ _ a b c _ => "Esc"
+ | RURule _ _ _ _ r => nd_urule2latex r
+ | RNote _ _ _ _ _ _ => "Note"
+ | RLit _ _ _ _ => "Lit"
+ | RVar _ _ _ _ => "Var"
+ | RGlobal _ _ _ _ _ => "Global"
+ | RLam _ _ _ _ _ _ => "Abs"
+ | RCast _ _ _ _ _ _ _ => "Cast"
+ | RAbsT _ _ _ _ _ _ => "AbsT"
+ | RAppT _ _ _ _ _ _ _ => "AppT"
+ | RAppCo _ _ _ _ _ _ _ _ _ => "AppCo"
+ | RAbsCo _ _ _ _ _ _ _ _ => "AbsCo"
+ | RApp _ _ _ _ _ _ _ => "App"
+ | RLet _ _ _ _ _ _ _ => "Let"
+ | RBindingGroup _ _ _ _ _ _ => "RBindingGroup"
+ | RLetRec _ _ _ _ _ _ => "LetRec"
+ | RCase _ _ _ _ _ _ _ _ => "Case"
+ | RBrak _ _ _ _ _ _ => "Brak"
+ | REsc _ _ _ _ _ _ => "Esc"
+ | REmptyGroup _ _ => "REmptyGroup"