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	25223	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	6205	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	3499	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	43061	log plain
-rw-r--r--	Ring_tac.v	14499	log plain
-rw-r--r--	Ring_theory.v	18407	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	5397	log plain
-rw-r--r--	newring.ml	39573	log plain
-rw-r--r--	newring.mli	1276	log plain
-rw-r--r--	newring_ast.mli	2030	log plain
-rw-r--r--	newring_plugin.mlpack	18	log plain