extraction « plugins - coq - the Coq proof assistant

Mode	Name	Size
-rw-r--r--	CHANGES	14095	log plain
-rw-r--r--	ExtrHaskellBasic.v	775	log plain
-rw-r--r--	ExtrHaskellNatInt.v	455	log plain
-rw-r--r--	ExtrHaskellNatInteger.v	462	log plain
-rw-r--r--	ExtrHaskellNatNum.v	1840	log plain
-rw-r--r--	ExtrHaskellString.v	1545	log plain
-rw-r--r--	ExtrHaskellZInt.v	843	log plain
-rw-r--r--	ExtrHaskellZInteger.v	853	log plain
-rw-r--r--	ExtrHaskellZNum.v	903	log plain
-rw-r--r--	ExtrOcamlBasic.v	1467	log plain
-rw-r--r--	ExtrOcamlBigIntConv.v	3850	log plain
-rw-r--r--	ExtrOcamlIntConv.v	3013	log plain
-rw-r--r--	ExtrOcamlNatBigInt.v	2696	log plain
-rw-r--r--	ExtrOcamlNatInt.v	3461	log plain
-rw-r--r--	ExtrOcamlString.v	1502	log plain
-rw-r--r--	ExtrOcamlZBigInt.v	3510	log plain
-rw-r--r--	ExtrOcamlZInt.v	3259	log plain
-rw-r--r--	Extraction.v	564	log plain
-rw-r--r--	README	4800	log plain
-rw-r--r--	big.ml	5811	log plain
-rw-r--r--	common.ml	21252	log plain
-rw-r--r--	common.mli	2919	log plain
-rw-r--r--	extract_env.ml	25522	log plain
-rw-r--r--	extract_env.mli	1372	log plain
-rw-r--r--	extraction.ml	40959	log plain
-rw-r--r--	extraction.mli	1264	log plain
-rw-r--r--	extraction_plugin.mlpack	90	log plain
-rw-r--r--	g_extraction.ml4	4645	log plain
-rw-r--r--	haskell.ml	13604	log plain
-rw-r--r--	haskell.mli	569	log plain
-rw-r--r--	json.ml	8103	log plain
-rw-r--r--	json.mli	39	log plain
-rw-r--r--	miniml.mli	6370	log plain
-rw-r--r--	mlutil.ml	49651	log plain
-rw-r--r--	mlutil.mli	4309	log plain
-rw-r--r--	modutil.ml	14402	log plain
-rw-r--r--	modutil.mli	1733	log plain
-rw-r--r--	ocaml.ml	26122	log plain
-rw-r--r--	ocaml.mli	567	log plain
-rw-r--r--	scheme.ml	7274	log plain
-rw-r--r--	scheme.mli	567	log plain
-rw-r--r--	table.ml	30611	log plain
-rw-r--r--	table.mli	7123	log plain