coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	Merge PR#432: [cleanup] Change Id.t option to Name.t in TacFun	Maxime Dénès	2017-03-14
\|\
* \|	Moving the Ltac plugin to a pack-based one.	Pierre-Marie Pédrot	2017-02-17
\| \| \| \| \| \| \| \| \| \| \| \| \| \|	This is cumbersome, because now code may fail at link time if it's not referring to the correct module name. Therefore, one has to add corresponding open statements a the top of every file depending on a Ltac module. This includes seemingly unrelated files that use EXTEND statements.
\| *	[cleanup] Change Id.t option to Name.t in TacFun	Tej Chajed	2017-02-16
\|/
*	Merge branch 'v8.6'	Pierre-Marie Pédrot	2017-01-19
\|\
\| *	ssrmatching: fix iter_constr_LR iterator wrt Proj	Enrico Tassi	2016-12-07
\| \|
* \|	Merge branch 'v8.6'	Pierre-Marie Pédrot	2016-12-07
\|\\|
\| *	ssrmatching: handle primite projections (fix: #5247)	Enrico Tassi	2016-12-05
\| \|
* \|	Merge branch 'v8.6'	Pierre-Marie Pédrot	2016-11-18
\|\\|
\| *	Merge commit 'e6edb33' into v8.6	Maxime Dénès	2016-11-07
\| \|\ \| \| \| \| \| \| \| \| \|	Was PR#331: Solve_constraints and Set Use Unification Heuristics
* \| \|	Merge branch 'v8.6'	Pierre-Marie Pédrot	2016-10-29
\|\\| \|
\| * \|	Merge remote-tracking branch 'github/pr/319' into v8.6	Maxime Dénès	2016-10-28
\| \|\ \ \| \| \| \| \| \| \| \| \| \| \| \|	Was PR#319: More error tagging, try to fix bug 5135
* \| \| \|	Merge branch 'v8.6'	Pierre-Marie Pédrot	2016-10-24
\|\\| \| \|
\| * \| \|	ssrmatching: fix interpretation of rpattern	Enrico Tassi	2016-10-24
\| \| \| \|
\| \| \| *	Renamings to avoid confusion deprecating old names	Matthieu Sozeau	2016-10-22
\| \| \|/ \| \|/\| \| \| \| \| \| \| \| \| \|	reconsider_conv_pbs -> reconsider_unif_constraints consider_remaining_unif_problems -> solve_unif_constraints_with_heuristics
\| \| *	[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	2016-10-18
\| \|/ \| \| \| \| \| \| \| \| \| \| \| \| \| \|	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.
* \|	Merge branch 'v8.6'	Pierre-Marie Pédrot	2016-09-23
\|\\|
* \|	Merging Stdarg and Constrarg.	Pierre-Marie Pédrot	2016-09-21
\| \| \| \| \| \| \| \| \| \| \| \|	There was no reason to keep them separate since quite a long time. Historically, they were making Genarg depend or not on upper strata of the code, but since it was moved to lib/ this is not justified anymore.
\| *	Addressing OCaml compilation warnings.	Hugo Herbelin	2016-09-16
\| \| \| \| \| \| \| \|	One of them revealed a true bug.
* \|	Moving Ltac-specific generic arguments to their own file in the ltac/ folder.	Pierre-Marie Pédrot	2016-09-15
\| \|
* \|	Moving Ltac-specific parsing API to ltac/ folder.	Pierre-Marie Pédrot	2016-09-14
\| \|
* \|	Make the user_err header an optional parameter.	Emilio Jesus Gallego Arias	2016-08-19
\| \| \| \| \| \| \| \|	Suggested by @ppedrot
* \|	Remove errorlabstrm in favor of user_err	Emilio Jesus Gallego Arias	2016-08-19
\| \| \| \| \| \| \| \| \| \| \| \| \| \|	As noted by @ppedrot, the first is redundant. The patch is basically a renaming. We didn't make the component optional yet, but this could happen in a future patch.
* \|	Unify location handling of error functions.	Emilio Jesus Gallego Arias	2016-08-19
\|/ \| \| \| \| \| \| \| \| \| \| \| \| \|	In some cases prior to this patch, there were two cases for the same error function, one taking a location, the other not. We unify them by using an option parameter, in the line with recent changes in warnings and feedback. This implies a bit of clean up in some places, but more importantly, is the preparation for subsequent patches making `Loc.location` opaque, change that could be use to improve modularity and allow a more functional implementation strategy --- for example --- of the beautifier.
*	errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib ↵	Pierre Letouzey	2016-07-03
\| \| \| \| \| \|	module) For the moment, there is an Error module in compilers-lib/ocamlbytecomp.cm(x)a
*	ssrmatching: avoid warnings about redundant typing clauses in ARGUMENT EXTEND	Pierre Letouzey	2016-06-27
\| \| \| \| \| \| \| \| \|	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].
*	ssrmatching: giving proper credits to the original author(s)	Enrico Tassi	2016-06-15
\| \| \| \| \|	Following CeCILL-B 5.3.2, we are allowed to redistribute the software under the same license of Coq as long as we credit.
*	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	2016-06-15
\| \| \| \|	for uniformity with other Debug options.
*	port ssrmatching plugin to the new makefile	Enrico Tassi	2016-06-14
\|
*	Ssreflect pattern matching facilities	Enrico Tassi	2016-03-02