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

Mode	Name	Size
-rw-r--r--	Array.v	836	log plain
-rw-r--r--	Char.v	680	log plain
-rw-r--r--	Constr.v	3079	log plain
-rw-r--r--	Control.v	3405	log plain
-rw-r--r--	Env.v	1394	log plain
-rw-r--r--	Fresh.v	1054	log plain
-rw-r--r--	Ident.v	795	log plain
-rw-r--r--	Init.v	2094	log plain
-rw-r--r--	Int.v	980	log plain
-rw-r--r--	Ltac1.v	1686	log plain
-rw-r--r--	Ltac2.v	860	log plain
-rw-r--r--	Message.v	1196	log plain
-rw-r--r--	Notations.v	16159	log plain
-rw-r--r--	Pattern.v	5375	log plain
-rw-r--r--	Std.v	10322	log plain
-rw-r--r--	String.v	838	log plain
-rw-r--r--	g_ltac2.mlg	29926	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	45545	log plain
-rw-r--r--	tac2core.mli	945	log plain
-rw-r--r--	tac2dyn.ml	951	log plain
-rw-r--r--	tac2dyn.mli	1215	log plain
-rw-r--r--	tac2entries.ml	30412	log plain
-rw-r--r--	tac2entries.mli	2987	log plain
-rw-r--r--	tac2env.ml	8224	log plain
-rw-r--r--	tac2env.mli	4946	log plain
-rw-r--r--	tac2expr.mli	5303	log plain
-rw-r--r--	tac2extffi.ml	1427	log plain
-rw-r--r--	tac2extffi.mli	677	log plain
-rw-r--r--	tac2ffi.ml	9454	log plain
-rw-r--r--	tac2ffi.mli	5773	log plain
-rw-r--r--	tac2intern.ml	51264	log plain
-rw-r--r--	tac2intern.mli	1900	log plain
-rw-r--r--	tac2interp.ml	7297	log plain
-rw-r--r--	tac2interp.mli	1260	log plain
-rw-r--r--	tac2match.ml	8836	log plain
-rw-r--r--	tac2match.mli	1201	log plain
-rw-r--r--	tac2print.ml	15968	log plain
-rw-r--r--	tac2print.mli	1561	log plain
-rw-r--r--	tac2qexpr.mli	4852	log plain
-rw-r--r--	tac2quote.ml	16625	log plain
-rw-r--r--	tac2quote.mli	3370	log plain
-rw-r--r--	tac2stdlib.ml	18107	log plain
-rw-r--r--	tac2stdlib.mli	590	log plain
-rw-r--r--	tac2tactics.ml	15307	log plain
-rw-r--r--	tac2tactics.mli	4549	log plain
-rw-r--r--	tac2types.mli	2508	log plain