coq - The formal proof system

Age	Commit message (Collapse)	Author
2016-12-07	ssrmatching: fix iter_constr_LR iterator wrt Proj	Enrico Tassi

2016-12-05	ssrmatching: handle primite projections (fix: #5247)	Enrico Tassi

2016-11-07	Merge commit 'e6edb33' into v8.6	Maxime Dénès
	Was PR#331: Solve_constraints and Set Use Unification Heuristics
2016-10-28	Merge remote-tracking branch 'github/pr/319' into v8.6	Maxime Dénès
	Was PR#319: More error tagging, try to fix bug 5135
2016-10-24	ssrmatching: fix interpretation of rpattern	Enrico Tassi

2016-10-22	Renamings to avoid confusion deprecating old names	Matthieu Sozeau
	reconsider_conv_pbs -> reconsider_unif_constraints consider_remaining_unif_problems -> solve_unif_constraints_with_heuristics
2016-10-18	[pp] Use more convenient pp API in ssrmatching	Emilio Jesus Gallego Arias

2016-10-18	[pp] Add tagging function to all low-level printing calls.	Emilio Jesus Gallego Arias
	The current tag system in `Pp` is generic, which implies we must choose a tagging function when calling a printer. For console printing there is a single choice, thus this commits adds it a few missing cases.
2016-09-16	Addressing OCaml compilation warnings.	Hugo Herbelin
	One of them revealed a true bug.
2016-07-03	errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib ↵	Pierre Letouzey
	module) For the moment, there is an Error module in compilers-lib/ocamlbytecomp.cm(x)a
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