setoid_ring « plugins - coq - the Coq proof assistant

Mode	Name	Size
-rw-r--r--	Algebra_syntax.v	924	log plain
-rw-r--r--	ArithRing.v	1783	log plain
-rw-r--r--	BinList.v	2208	log plain
-rw-r--r--	Cring.v	8982	log plain
-rw-r--r--	Field.v	581	log plain
-rw-r--r--	Field_tac.v	19572	log plain
-rw-r--r--	Field_theory.v	53831	log plain
-rw-r--r--	InitialRing.v	25244	log plain
-rw-r--r--	Integral_domain.v	1304	log plain
-rw-r--r--	NArithRing.v	769	log plain
-rw-r--r--	Ncring.v	9480	log plain
-rw-r--r--	Ncring_initial.v	6171	log plain
-rw-r--r--	Ncring_polynom.v	16994	log plain
-rw-r--r--	Ncring_tac.v	9439	log plain
-rw-r--r--	RealField.v	3239	log plain
-rw-r--r--	Ring.v	1454	log plain
-rw-r--r--	Ring_base.v	817	log plain
-rw-r--r--	Ring_polynom.v	43066	log plain
-rw-r--r--	Ring_tac.v	14545	log plain
-rw-r--r--	Ring_theory.v	18420	log plain
-rw-r--r--	Rings_Q.v	779	log plain
-rw-r--r--	Rings_R.v	919	log plain
-rw-r--r--	Rings_Z.v	328	log plain
-rw-r--r--	ZArithRing.v	1542	log plain
-rw-r--r--	g_newring.ml4	4173	log plain
-rw-r--r--	newring.ml	37794	log plain
-rw-r--r--	newring.mli	2260	log plain
-rw-r--r--	newring_ast.mli	2032	log plain
-rw-r--r--	newring_plugin.mlpack	18	log plain
-rw-r--r--	vo.itarget	320	log plain