coq - The formal proof system

Age	Commit message (Collapse)	Author
2016-06-27	ssrmatching: avoid warnings about redundant typing clauses in ARGUMENT EXTEND	Pierre Letouzey
	The warnings were: Redundant [RAW_TYPED AS] clause in [ARGUMENT EXTEND cpattern]. Redundant [GLOB_TYPED AS] clause in [ARGUMENT EXTEND cpattern]. Redundant [RAW_TYPED AS] clause in [ARGUMENT EXTEND lcpattern]. Redundant [GLOB_TYPED AS] clause in [ARGUMENT EXTEND lcpattern].
2016-06-15	ssrmatching: giving proper credits to the original author(s)	Enrico Tassi
	Following CeCILL-B 5.3.2, we are allowed to redistribute the software under the same license of Coq as long as we credit.
2016-06-15	ssrmatching: ltac argument parsing made more robust	Enrico Tassi

2016-06-15	ssrmatching: debug prints sent via msg_debug	Enrico Tassi

2016-06-15	Rename "Set SsrMatchingDebug" into "Set Debug SsrMatching"	Enrico Tassi
	for uniformity with other Debug options.
2016-06-14	port ssrmatching plugin to the new makefile	Enrico Tassi

2016-03-02	Ssreflect pattern matching facilities	Enrico Tassi