Ltac2 « user-contrib - coq - The formal proof system

Mode	Name	Size
-rw-r--r--	Array.v	9151	log plain
-rw-r--r--	Bool.v	1419	log plain
-rw-r--r--	Char.v	830	log plain
-rw-r--r--	Constr.v	3876	log plain
-rw-r--r--	Control.v	4278	log plain
-rw-r--r--	Env.v	1544	log plain
-rw-r--r--	Fresh.v	1383	log plain
-rw-r--r--	Ident.v	945	log plain
-rw-r--r--	Init.v	2538	log plain
-rw-r--r--	Int.v	1604	log plain
-rw-r--r--	List.v	15720	log plain
-rw-r--r--	Ltac1.v	1836	log plain
-rw-r--r--	Ltac2.v	1010	log plain
-rw-r--r--	Message.v	1346	log plain
-rw-r--r--	Notations.v	17796	log plain
-rw-r--r--	Option.v	1643	log plain
-rw-r--r--	Pattern.v	5525	log plain
-rw-r--r--	Std.v	10471	log plain
-rw-r--r--	String.v	988	log plain
-rw-r--r--	dune	322	log plain
-rw-r--r--	g_ltac2.mlg	30987	log plain
-rw-r--r--	ltac2_plugin.mlpack	139	log plain
-rw-r--r--	plugin_base.dune	190	log plain
-rw-r--r--	tac2core.ml	53567	log plain
-rw-r--r--	tac2core.mli	1095	log plain
-rw-r--r--	tac2dyn.ml	1101	log plain
-rw-r--r--	tac2dyn.mli	1365	log plain
-rw-r--r--	tac2entries.ml	32315	log plain
-rw-r--r--	tac2entries.mli	3304	log plain
-rw-r--r--	tac2env.ml	8608	log plain
-rw-r--r--	tac2env.mli	5429	log plain
-rw-r--r--	tac2expr.mli	5528	log plain
-rw-r--r--	tac2extffi.ml	1577	log plain
-rw-r--r--	tac2extffi.mli	827	log plain
-rw-r--r--	tac2ffi.ml	9982	log plain
-rw-r--r--	tac2ffi.mli	6194	log plain
-rw-r--r--	tac2intern.ml	54240	log plain
-rw-r--r--	tac2intern.mli	2103	log plain
-rw-r--r--	tac2interp.ml	7840	log plain
-rw-r--r--	tac2interp.mli	1410	log plain
-rw-r--r--	tac2match.ml	9118	log plain
-rw-r--r--	tac2match.mli	1351	log plain
-rw-r--r--	tac2print.ml	16029	log plain
-rw-r--r--	tac2print.mli	1711	log plain
-rw-r--r--	tac2qexpr.mli	5002	log plain
-rw-r--r--	tac2quote.ml	17701	log plain
-rw-r--r--	tac2quote.mli	3672	log plain
-rw-r--r--	tac2stdlib.ml	18257	log plain
-rw-r--r--	tac2stdlib.mli	740	log plain
-rw-r--r--	tac2tactics.ml	15528	log plain
-rw-r--r--	tac2tactics.mli	4699	log plain
-rw-r--r--	tac2types.mli	2658	log plain