coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	Merge branch 'v8.6'	Pierre-Marie Pédrot	2016-10-05
\|\
\| *	fixing bug 4609: document an option governing the generation of equalities	Yves Bertot	2016-10-03
\| \| \| \| \| \| \| \|	between proofs in tactic injection, with a side-effect on inversion.
* \|	Merge branch 'v8.6'	Pierre-Marie Pédrot	2016-10-02
\|\\|
\| *	Merge remote-tracking branch 'github/pr/280' into v8.6	Maxime Dénès	2016-09-30
\| \|\ \| \| \| \| \| \| \| \| \| \| \| \|	Was PR#280: Document that [Reset Ltac Profile] is not synchronized with the document state
\| * \	Merge branch 'v8.5' into v8.6	Maxime Dénès	2016-09-30
\| \|\ \
\| * \ \	Merge remote-tracking branch 'github/pr/232' into v8.6	Maxime Dénès	2016-09-28
\| \|\ \ \ \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Was PR#232: Fix the parsing of goal selectors.
\| \| \| * \|	Fixing #4887 (confusion between using and with in documentation of firstorder).	Hugo Herbelin	2016-09-27
\| \| \| \| \|
* \| \| \| \|	Merge branch 'v8.6'	Pierre-Marie Pédrot	2016-09-23
\|\\| \| \| \|
\| * \| \| \|	Merge branch 'v8.5' into v8.6	Pierre-Marie Pédrot	2016-09-23
\| \|\ \ \ \ \| \| \| \|/ / \| \| \|/\| \|
\| \| * \| \|	Replace { command ; } with ( command )	Erik Martin-Dorel	2016-09-19
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	as suggested by Hugo. Also, escape the spaces after the dots to obtain a better PdfLaTeX output.
\| \| * \| \|	Fix typos in RefMan-uti.tex.	Erik Martin-Dorel	2016-09-19
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	- Ensure "coq_makefile --help" is properly typeset with HeVeA/PdfLaTeX - Replace 's with "s so they are typeset as true ASCII characters - Add missing ; before closing brace.
\| \| \| \| *	Doc: [Reset Ltac Profile] is not synchronized	Jason Gross	2016-09-16
\| \| \|_\|/ \| \|/\| \|
\| * \| \|	Extending "contradiction" so that it recognizes statements such as "~x=x" or ↵	Hugo Herbelin	2016-09-15
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	~True. Found 1 incompatibility in tested contribs and 3 times the same pattern of incompatibility in the standard library. In all cases, it is an improvement in the form of the script. New behavior deactivated when version is <= 8.5.
* \| \| \|	Merge branch 'v8.6'	Pierre-Marie Pédrot	2016-09-14
\|\\| \| \|
\| * \| \|	Refolding: disable in 8.4 compat file, document	Matthieu Sozeau	2016-09-12
\| \| \| \|
* \| \| \|	Merge PR #244.	Pierre-Marie Pédrot	2016-09-08
\|\ \ \ \
\| \| * \| \|	Fix a typo in the reference manual	Jason Gross	2016-09-07
\| \|/ / / \|/\| \| \|
* \| \| \|	plugin micromega : nra also handles non-linear rational arithmetic over Q ↵	Frédéric Besson	2016-08-30
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	(Fixed #4985) Lqa.v defines the tactics lra and nra working over Q. Lra.v defines the tactics lra and nra working over R.
* \| \| \|	update Proof General URL	Paul Steckler	2016-08-23
\| \| \| \|
* \| \| \|	Documenting "Set Structural Injection".	Hugo Herbelin	2016-08-21
\| \| \| \|
\| * \| \|	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.
* \| \| \|	In docs, fix command to reset Ltac profiling	Paul Steckler	2016-08-17
\|/ / /
* \| \|	Merge branch 'v8.5' into v8.6	Pierre-Marie Pédrot	2016-08-16
\|\\| \|
\| * \|	Fix documentation typo (bug #4994).	Guillaume Melquiond	2016-08-04
\| \| \|
* \| \|	More examples of recursive notations, with emphasis in reference manual.	Hugo Herbelin	2016-07-17
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Further work would include: - Identify binders up to alpha-conversion (see #4932 with a list of binders of length at least 2, or #4592 on printing notations such as ex2). A cool example that one could also consider supporting: - Notation "[[ a , .. , b \| .. \| a , .. , b ]]" := (cons (cons a .. (cons b nil) ..) .. (cons a .. (cons b nil) ..) ..).
* \| \|	Add and document match, fix and cofix reduction flags.	Maxime Dénès	2016-07-01
\| \| \|
\| \| *	Update the documentation for goal selectors.	Cyprien Mangin	2016-06-30
\| \|/ \|/\|
* \|	Updated CHANGES about subst. More on recursive equations in reference manual.	Hugo Herbelin	2016-06-29
\| \|
* \|	Fixes in documentation.	Matthieu Sozeau	2016-06-29
\| \|
* \|	Program: cleanup in cases, add options	Matthieu Sozeau	2016-06-29
\| \| \| \| \| \| \| \| \| \| \| \| \| \|	Unset Program Generalized Coercion to avoid coercion of general applications. Unset Program Cases to deactivate generation equalities and disequalities of cases.
* \|	Merge remote-tracking branch 'github/pr/207' into trunk	Maxime Dénès	2016-06-28
\|\ \ \| \| \| \| \| \| \| \| \|	Was PR#207: Add -no-print-dependent-evars
* \| \|	Documenting the "only printing" notation flag.	Pierre-Marie Pédrot	2016-06-28
\| \| \|
* \| \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2016-06-27
\|\ \ \ \| \| \|/ \| \|/\|
* \| \|	Adding ability to put any pattern in binders, prefixed by a quote.	Daniel de Rauglaudre	2016-06-27
\| \| \| \| \| \| \| \| \| \| \| \|	Cf CHANGES for details.
\| * \|	Reference Manual / Extraction: the original example command no longer works ↵	Matej Kosik	2016-06-20
\| \| \| \| \| \| \| \| \| \| \| \|	with recent Coq
\| \| *	Add [Unset Printing Dependent Evars Line]	Jason Gross	2016-06-19
\| \|/ \|/\| \| \| \| \| \| \|	This allows a work-around for bug #4819, https://coq.inria.fr/bugs/show_bug.cgi?id=4819.
* \|	par: like all: but in parallel	Enrico Tassi	2016-06-17
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	This commit documents par:, fixes its semantics so that is behaves like all:, supports (toplevel) abstract and optimizes toplevel solve. `par: solve [tac]` is equivalent to `Ltac tac1 := solve[tac]...par: tac1` but is optimized for failures: if one goal fails all are aborted immediately. `par: abstract tac` runs abstract on the generated proof terms. Nested abstract calls are not supported.
* \|	Document new Hint Mode option.	Matthieu Sozeau	2016-06-16
\| \|
* \|	Revise syntax of Hint Cut	Matthieu Sozeau	2016-06-16
\| \| \| \| \| \| \| \| \| \|	As noticed by C. Cohen it was confusingly different from standard notation.
* \|	Merge 'pr/191' into trunk	Enrico Tassi	2016-06-16
\|\ \
* \| \|	typography	Matej Kosik	2016-06-15
\| \| \|
\| * \|	Add documentation for goal selectors.	Cyprien Mangin	2016-06-14
\| \| \|
* \| \|	-async-proofs-delegation-threshold default value set to 0.03	Enrico Tassi	2016-06-14
\| \| \| \| \| \| \| \| \| \| \| \|	Documentation also updated.
* \| \|	Merge remote-tracking branch 'origin/pr/173' into trunk	Enrico Tassi	2016-06-14
\|\ \ \ \| \|/ / \|/\| \| \| \| \|	This is the "error resiliency" mode for STM
* \| \|	Merge branch "LtacProf for trunk" (PR #165).	Pierre-Marie Pédrot	2016-06-14
\|\ \ \
* \| \| \|	Univs: more robust Universe/Constraint decls #4816	Matthieu Sozeau	2016-06-13
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	This fixes the declarations of constraints, universes and assumptions: - global constraints can refer to global universes only, - polymorphic universes, constraints and assumptions can only be declared inside sections, when all the section's variables/universes are polymorphic as well. - monomorphic assumptions may only be declared in section contexts which are not parameterized by polymorphic universes/assumptions. Add fix for part 1 of bug #4816
* \| \| \|	typo	Matej Kosik	2016-06-07
\| \| \| \|
* \| \| \|	typography	Matej Kosik	2016-06-07
\| \| \| \|
\| \| * \|	Documentation	Enrico Tassi	2016-06-07
\| \|/ / \|/\| \|
\| * \|	Make Ltac Profiling an setting	Jason Gross	2016-06-05
\| \| \|