coq - The formal proof system

Age	Commit message (Collapse)	Author
2017-08-21	Ensuring all .v files end with a newline to make "sed -i" work better on them.	Hugo Herbelin

2017-06-14	Prelude : no more autoload of plugins extraction and recdef	Pierre Letouzey
	The user now has to manually load them, respectively via: Require Extraction Require Import FunInd The "Import" in the case of FunInd is to ensure that the tactics functional induction and functional inversion are indeed in scope. Note that the Recdef.v file is still there as well (it contains complements used when doing Function with measures), and it also triggers a load of FunInd.v. This change is correctly documented in the refman, and the test-suite has been adapted.
2015-09-03	Improve directives for Haskell extraction of nat.	Maxime Dénès

2015-09-03	Fix [Nat.div] and add [Nat.modulo] in ExtrHaskellNatNum.v	Nickolai Zeldovich
	The previous extraction of [Nat.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 [Nat.modulo], with the same check for modulo-by-zero.
2015-06-22	Add efficient extraction of [nat], [Z], and [string] to Haskell	Nickolai Zeldovich
	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