coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	[option] Remove support for non-synchronous options.	Emilio Jesus Gallego Arias	2017-05-24
\| \| \| \| \| \| \| \| \| \| \| \|	Inspired by https://coq.inria.fr/bugs/show_bug.cgi?id=5229 , which this PR solves, I propose to remove support for non-synchronous options. It seems the few uses of `optsync = false` we legacy and shouldn't have any impact. Moreover, non synchronous options may create particularly tricky situations as for instance, they won't be propagated to workers.
*	Remove unused [open] statements	Gaetan Gilbert	2017-04-27
\|
*	Remove unused constructors	Gaetan Gilbert	2017-04-27
\|
*	Remove some unused values and types	Gaetan Gilbert	2017-04-27
\|
*	Fix omitted labels in function calls	Gaetan Gilbert	2017-04-27
\|
*	Merge PR#379: Introducing evar-insensitive constrs	Maxime Dénès	2017-04-11
\|\
* \|	[camlpX] Remove camlp4 compat layer.	Emilio Jesus Gallego Arias	2017-04-07
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	We remove the camlp4 compatibility layer, and try to clean up most structures. `parsing/compat` is gone. We added some documentation to the lexer/parser interfaces that are often obscured by module includes.
\| *	Merge branch 'trunk' into pr379	Maxime Dénès	2017-04-04
\| \|\ \| \|/ \|/\|
\| *	Merge branch 'trunk' into pr379	Maxime Dénès	2017-03-24
\| \|\
* \| \|	Replacing "cast surgery" in LetIn by a proper field (see PR #404).	Hugo Herbelin	2017-03-24
\| \|/ \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	This is a patch fulfilling the relevant remark of Maxime that an explicit information at the ML type level would be better than "cast surgery" to carry the optional type of a let-in. There are a very few semantic changes. - a "(x:t:=c)" in a block of binders is now written in the more standard way "(x:=c:t)" - in notations, the type of a let-in is not displayed if not explicitly asked so. See discussion at PR #417 for more information.
* \|	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 'master'.	Pierre-Marie Pédrot	2017-02-14
\| \|\ \| \|/ \|/\|
\| *	Porting the ssrmatching plugin to the new EConstr API.	Enrico Tassi	2017-02-14
\| \|
\| *	Definining EConstr-based contexts.	Pierre-Marie Pédrot	2017-02-14
\| \| \| \| \| \| \| \| \| \| \| \|	This removes quite a few unsafe casts. Unluckily, I had to reintroduce the old non-module based names for these data structures, because I could not reproduce easily the same hierarchy in EConstr.
\| *	Evar-normalizing functions now act on EConstrs.	Pierre-Marie Pédrot	2017-02-14
\| \|
\| *	Removing various compatibility layers of tactics.	Pierre-Marie Pédrot	2017-02-14
\| \|
\| *	Ltac now uses evar-based constrs.	Pierre-Marie Pédrot	2017-02-14
\| \|
\| *	Removing compatibility layers in Retyping	Pierre-Marie Pédrot	2017-02-14
\| \|
\| *	Proofview.Goal primitive now return EConstrs.	Pierre-Marie Pédrot	2017-02-14
\| \|
\| *	Tactics API using EConstr.	Pierre-Marie Pédrot	2017-02-14
\| \|
\| *	Tacmach API using EConstr.	Pierre-Marie Pédrot	2017-02-14
\| \|
\| *	Goal API using EConstr.	Pierre-Marie Pédrot	2017-02-14
\| \|
\| *	Unification API using EConstr.	Pierre-Marie Pédrot	2017-02-14
\| \|
\| *	Tacred API using EConstr.	Pierre-Marie Pédrot	2017-02-14
\| \|
\| *	Evarconv API using EConstr.	Pierre-Marie Pédrot	2017-02-14
\| \|
\| *	Reductionops API using EConstr.	Pierre-Marie Pédrot	2017-02-14
\| \|
\| *	Termops API using EConstr.	Pierre-Marie Pédrot	2017-02-14
\| \|
* \|	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.