extraction « plugins - coq - The formal proof system

Mode	Name	Size
-rw-r--r--	CHANGES	14095	log plain
-rw-r--r--	ExtrOcamlBasic.v	1431	log plain
-rw-r--r--	ExtrOcamlBigIntConv.v	3814	log plain
-rw-r--r--	ExtrOcamlIntConv.v	2977	log plain
-rw-r--r--	ExtrOcamlNatBigInt.v	2661	log plain
-rw-r--r--	ExtrOcamlNatInt.v	3102	log plain
-rw-r--r--	ExtrOcamlString.v	1466	log plain
-rw-r--r--	ExtrOcamlZBigInt.v	3475	log plain
-rw-r--r--	ExtrOcamlZInt.v	3047	log plain
-rw-r--r--	README	4802	log plain
-rw-r--r--	big.ml	5811	log plain
-rw-r--r--	common.ml	20010	log plain
-rw-r--r--	common.mli	2962	log plain
-rw-r--r--	extract_env.ml	21364	log plain
-rw-r--r--	extract_env.mli	1116	log plain
-rw-r--r--	extraction.ml	39146	log plain
-rw-r--r--	extraction.mli	1149	log plain
-rw-r--r--	extraction_plugin.mllib	107	log plain
-rw-r--r--	g_extraction.ml4	4057	log plain
-rw-r--r--	haskell.ml	12057	log plain
-rw-r--r--	haskell.mli	569	log plain
-rw-r--r--	miniml.mli	6357	log plain
-rw-r--r--	mlutil.ml	43157	log plain
-rw-r--r--	mlutil.mli	4236	log plain
-rw-r--r--	modutil.ml	13728	log plain
-rw-r--r--	modutil.mli	1605	log plain
-rw-r--r--	ocaml.ml	25717	log plain
-rw-r--r--	ocaml.mli	567	log plain
-rw-r--r--	scheme.ml	7160	log plain
-rw-r--r--	scheme.mli	567	log plain
-rw-r--r--	table.ml	28528	log plain
-rw-r--r--	table.mli	6612	log plain
-rw-r--r--	vo.itarget	157	log plain