| Commit message (Collapse) | Author | Age | |
|---|---|---|---|
| * | Fix [Z.div] and add [Z.modulo] in ExtrHaskellZNum.v |  Nickolai Zeldovich | 2015-09-03 |
| | | | | | | | | | | The previous extraction of [Z.div] for Haskell did not properly handle divide-by-zero. Fix it by introducing an explicit [if] statement in the generated Haskell code. Also, introduce a similar extraction rule for [Z.modulo], with the same check for modulo-by-zero. | ||
| * | Add efficient extraction of [nat], [Z], and [string] to Haskell | Nickolai Zeldovich | 2015-06-22 |
| This mirrors the existing extraction libraries for OCaml. One wart: the extraction for [string] requires that the Haskell code imports Data.Bits and Data.Char. Coq has no way to add extra import statements to the extracted code. So we have to rely on the user to somehow import these libraries (e.g., using the -pgmF ghc option). See also https://coq.inria.fr/bugs/show_bug.cgi?id=4189 Message to github robot: this commit closes #65 | |||
 |
index : coq | |
| the Coq proof assistant |
| aboutsummaryrefslogtreecommitdiffhomepage |