extraction « plugins - coq - The formal proof system

Mode	Name	Size
-rw-r--r--	CHANGES	14098	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	1841	log plain
-rw-r--r--	ExtrHaskellString.v	4555	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	1617	log plain
-rw-r--r--	ExtrOcamlBigIntConv.v	4000	log plain
-rw-r--r--	ExtrOcamlIntConv.v	3164	log plain
-rw-r--r--	ExtrOcamlNatBigInt.v	2834	log plain
-rw-r--r--	ExtrOcamlNatInt.v	3599	log plain
-rw-r--r--	ExtrOcamlString.v	4397	log plain
-rw-r--r--	ExtrOcamlZBigInt.v	3660	log plain
-rw-r--r--	ExtrOcamlZInt.v	3409	log plain
-rw-r--r--	Extraction.v	715	log plain
-rw-r--r--	README	4800	log plain
-rw-r--r--	big.ml	5985	log plain
-rw-r--r--	common.ml	21227	log plain
-rw-r--r--	common.mli	2925	log plain
-rw-r--r--	extract_env.ml	27395	log plain
-rw-r--r--	extract_env.mli	1619	log plain
-rw-r--r--	extraction.ml	47831	log plain
-rw-r--r--	extraction.mli	1521	log plain
-rw-r--r--	extraction_plugin.mlpack	97	log plain
-rw-r--r--	g_extraction.mlg	5265	log plain
-rw-r--r--	haskell.ml	13705	log plain
-rw-r--r--	haskell.mli	719	log plain
-rw-r--r--	json.ml	8219	log plain
-rw-r--r--	json.mli	39	log plain
-rw-r--r--	miniml.ml	6345	log plain
-rw-r--r--	miniml.mli	6347	log plain
-rw-r--r--	mlutil.ml	50722	log plain
-rw-r--r--	mlutil.mli	4430	log plain
-rw-r--r--	modutil.ml	14556	log plain
-rw-r--r--	modutil.mli	1847	log plain
-rw-r--r--	ocaml.ml	27550	log plain
-rw-r--r--	ocaml.mli	717	log plain
-rw-r--r--	plugin_base.dune	146	log plain
-rw-r--r--	scheme.ml	7515	log plain
-rw-r--r--	scheme.mli	717	log plain
-rw-r--r--	table.ml	29921	log plain
-rw-r--r--	table.mli	7114	log plain