setoid_ring « plugins - coq - The formal proof system

Mode	Name	Size
-rw-r--r--	Algebra_syntax.v	1599	log plain
-rw-r--r--	ArithRing.v	2283	log plain
-rw-r--r--	BinList.v	2358	log plain
-rw-r--r--	Cring.v	9160	log plain
-rw-r--r--	Field.v	731	log plain
-rw-r--r--	Field_tac.v	19722	log plain
-rw-r--r--	Field_theory.v	55513	log plain
-rw-r--r--	InitialRing.v	26884	log plain
-rw-r--r--	Integral_domain.v	1980	log plain
-rw-r--r--	NArithRing.v	919	log plain
-rw-r--r--	Ncring.v	9630	log plain
-rw-r--r--	Ncring_initial.v	6378	log plain
-rw-r--r--	Ncring_polynom.v	17167	log plain
-rw-r--r--	Ncring_tac.v	9751	log plain
-rw-r--r--	RealField.v	4318	log plain
-rw-r--r--	Ring.v	1604	log plain
-rw-r--r--	Ring_base.v	945	log plain
-rw-r--r--	Ring_polynom.v	43736	log plain
-rw-r--r--	Ring_tac.v	15702	log plain
-rw-r--r--	Ring_theory.v	19163	log plain
-rw-r--r--	Rings_Q.v	1464	log plain
-rw-r--r--	Rings_R.v	1604	log plain
-rw-r--r--	Rings_Z.v	1004	log plain
-rw-r--r--	ZArithRing.v	1692	log plain
-rw-r--r--	g_newring.mlg	4952	log plain
-rw-r--r--	newring.ml	37559	log plain
-rw-r--r--	newring.mli	1293	log plain
-rw-r--r--	newring_ast.ml	2258	log plain
-rw-r--r--	newring_ast.mli	2258	log plain
-rw-r--r--	newring_plugin.mlpack	30	log plain
-rw-r--r--	plugin_base.dune	141	log plain