projects
/
coq-hetmet.git
/ blobdiff
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
|
commitdiff
|
tree
raw
|
inline
| side by side
Added WeakVar, a separate variable representation for HaskWeak
[coq-hetmet.git]
/
src
/
Extraction-prefix.hs
diff --git
a/src/Extraction-prefix.hs
b/src/Extraction-prefix.hs
index
68c40e5
..
595b8d1
100644
(file)
--- a/
src/Extraction-prefix.hs
+++ b/
src/Extraction-prefix.hs
@@
-36,7
+36,8
@@
import qualified Data.Char
import Data.Bits ((.&.), shiftL, (.|.))
import Prelude ( (++), (+), (==), Show, show, Char )
import Data.Bits ((.&.), shiftL, (.|.))
import Prelude ( (++), (+), (==), Show, show, Char )
-{-
+dataConEqTheta' dc = map (\p -> {-FIXME-}) (DataCon.dataConEqTheta dc)
+
nat2int :: Nat -> Prelude.Int
nat2int O = 0
nat2int (S x) = 1 + (nat2int x)
nat2int :: Nat -> Prelude.Int
nat2int O = 0
nat2int (S x) = 1 + (nat2int x)
@@
-74,4
+75,4
@@
coreVarSort v | otherwise = Prelude.error "Var.Var that is neither an expres
outputableToString :: Outputable -> String
outputableToString = (\x -> Outputable.showSDoc (Outputable.ppr x))
outputableToString :: Outputable -> String
outputableToString = (\x -> Outputable.showSDoc (Outputable.ppr x))
--}
+