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	2283	log plain
-rw-r--r--	BinList.v	2358	log plain
-rw-r--r--	Cring.v	9132	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	54489	log plain
-rw-r--r--	InitialRing.v	26874	log plain
-rw-r--r--	Integral_domain.v	1304	log plain
-rw-r--r--	NArithRing.v	919	log plain
-rw-r--r--	Ncring.v	9630	log plain
-rw-r--r--	Ncring_initial.v	6355	log plain
-rw-r--r--	Ncring_polynom.v	17144	log plain
-rw-r--r--	Ncring_tac.v	9589	log plain
-rw-r--r--	RealField.v	3499	log plain
-rw-r--r--	Ring.v	1604	log plain
-rw-r--r--	Ring_base.v	967	log plain
-rw-r--r--	Ring_polynom.v	43391	log plain
-rw-r--r--	Ring_tac.v	15048	log plain
-rw-r--r--	Ring_theory.v	19173	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	1692	log plain
-rw-r--r--	g_newring.ml4	5672	log plain
-rw-r--r--	newring.ml	39921	log plain
-rw-r--r--	newring.mli	1426	log plain
-rw-r--r--	newring_ast.mli	2182	log plain
-rw-r--r--	newring_plugin.mlpack	18	log plain