X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=blobdiff_plain;f=src%2FHaskLiteralsAndTyCons.v;h=38e7f95c84297c52a84e343f316682a849b459b4;hp=62d638bbdcf753588d513ed02c1828985156ecdb;hb=75a0b52b9937ab6b68ed98cc24281bc9153e96b9;hpb=d4b00db15359657e07a36167b2a28882460fdd8f

diff --git a/src/HaskLiteralsAndTyCons.v b/src/HaskLiteralsAndTyCons.v
index 62d638b..38e7f95 100644
--- a/src/HaskLiteralsAndTyCons.v
+++ b/src/HaskLiteralsAndTyCons.v
@@ -90,4 +90,6 @@ Instance TyConToLatex    : ToLatex  TyCon := { toLatex  := fun x => toLatex (toS
 Instance TyFunToLatex    : ToLatex  TyCon := { toLatex  := fun x => toLatex (toString x) }.
 
 Variable ModalBoxTyCon   : TyCon.        Extract Inlined Constant ModalBoxTyCon => "TysWiredIn.hetMetCodeTypeTyCon".
+Variable PairTyCon       : TyFun.        Extract Inlined Constant PairTyCon     => "TysWiredIn.pairTyCon".
+Variable UnitTyCon       : TyFun.        Extract Inlined Constant UnitTyCon     => "TysWiredIn.unitTyCon".
 Variable ArrowTyCon      : TyCon.        Extract Constant ArrowTyCon    => "Type.funTyCon".