coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	Chaining two tactics in a proof	Raphaël Monat	2017-10-27
\|
*	Moving from `is_true` to `= true`	Raphaël Monat	2017-10-25
\|
*	Added proofs of Qeq_bool_refl, Qeq_bool_sym, Qeq_bool_trans.	Raphaël Monat	2017-10-12
\|
*	Changed Qeq_bool_sym into Qeq_bool_comm, used the proof of @letouzey.	Raphaël Monat	2017-10-08
\|
*	Removed leb_not_le (already existing as Nat.leb_nle)	Raphaël Monat	2017-10-08
\|
*	Changed the statement of leb_not_le; shortened the proof	Raphaël Monat	2017-10-03
\|
*	Merge branch 'master' of https://github.com/coq/coq	Raphaël Monat	2017-10-03
\|\
* \|	Add Qabs_Qinv: Qabs (/ q) == / (Qabs q).	Raphaël Monat	2017-10-03
\| \|
* \|	Add Qeq_bool_sym: Qeq_bool x y = Qeq_bool y x.	Raphaël Monat	2017-10-03
\| \|
* \|	Add leb_not_le: (n <=? m) = false -> n > m.	Raphaël Monat	2017-10-03
\| \|
\| *	Merge PR #1110: Mention requiring extraction/funind in CHANGES	Maxime Dénès	2017-10-03
\| \|\
\| * \	Merge PR #1105: [stm] Remove unused "Proof using" data in `Sync` tags.	Maxime Dénès	2017-10-03
\| \|\ \
\| * \ \	Merge PR #1104: Browser userscript to turn BZ#XXXX occurences into links.	Maxime Dénès	2017-10-03
\| \|\ \ \
\| * \ \ \	Merge PR #1100: Avoid looping when searching for CoqProject.	Maxime Dénès	2017-10-03
\| \|\ \ \ \
\| * \ \ \ \	Merge PR #1099: BZ#5637, look for Obligation num or Next Obligation to start ↵	Maxime Dénès	2017-10-03
\| \|\ \ \ \ \ \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	proof for coqwc
\| * \ \ \ \ \	Merge PR #1097: Properly display the "only" prefix for selectors (bug #5760).	Maxime Dénès	2017-10-03
\| \|\ \ \ \ \ \
\| * \ \ \ \ \ \	Merge PR #1094: Fixing a little parsing bug with level 90 introduced in ↵	Maxime Dénès	2017-10-03
\| \|\ \ \ \ \ \ \ \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	3e70ea9c.
\| * \ \ \ \ \ \ \	Merge PR #1090: [ide] Avoid duplicate error printing (BZ#5583)	Maxime Dénès	2017-10-03
\| \|\ \ \ \ \ \ \ \
\| * \| \| \| \| \| \| \| \|	Merge PR #1084: After testing it in live, writing metas using an ↵	Maxime Dénès	2017-10-03
\|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	?INTERNAL#42 style is ugly
* \| \| \| \| \| \| \| \| \|	Merge PR #1015: Adding a function to be typically used to pass values from ↵	Maxime Dénès	2017-10-03
\|\ \ \ \ \ \ \ \ \ \ \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	an OCaml "when" clause to the r.h.s of the matching clause
* \ \ \ \ \ \ \ \ \ \	Merge PR #1080: Remove some unused parts of the reference manual.	Maxime Dénès	2017-10-03
\|\ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \	Merge PR #1076: Properly handle "coq_makefile -Q . Foo" (bug #5580).	Maxime Dénès	2017-10-03
\|\ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \	Merge PR #1072: Do not run Travis OS X packaging job on PRs	Maxime Dénès	2017-10-03
\|\ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \	Merge PR #1040: Efficient fresh name generation	Maxime Dénès	2017-10-03
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \	Merge PR #1023: dev/build/windows/makecoq_mingw.sh: install camlp5's META file	Maxime Dénès	2017-10-03
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \	Merge PR #1019: Fix BZ#5655 by avoiding the creation of a cleaner thread for ↵	Maxime Dénès	2017-10-03
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	empty queues.
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \	Merge PR #1012: Make a test for coq_makefile portable.	Maxime Dénès	2017-10-03
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \	Merge PR #667: [vernac] Remove `Qed exporting` syntax.	Maxime Dénès	2017-10-03
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| *	Mention requiring extraction/funind in CHANGES	Tej Chajed	2017-10-02
\| \|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|/ \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| \| \| \| \| \| \| * \| \| \| \| \| \|	[ide] Avoid duplicate error printing (BZ#5583)	Emilio Jesus Gallego Arias	2017-09-29
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	See the discussion in the bug tracker, basically the STM delays the feedback error message to a point where CoqIDE has forgotten about the sentence, thus we were processing such errors in the generic case, printing them twice as the Fail case will also do it. We could indeed revert back to the 8.6 strategy for error (print always from Fail and ignore Feedback), however I feel that time will be better spent by fixing the STM than adding more CoqIDE workarounds.
\| * \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	[vernac] Remove `Qed exporting` syntax.	Emilio Jesus Gallego Arias	2017-09-29
\|/ / / / / / / / / / / / / / / / / \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	We don't gain anything from the kernel yet as transparent constants _do_ require the `side_eff` exporting machinery. Next step, understand why.
\| \| \| \| * \| \| \| \| \| \| \| \| \| \| \| \|	Efficient computation of the names contained in an environment.	Pierre-Marie Pédrot	2017-09-28
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| * \| \| \| \| \| \| \| \| \| \| \| \|	Efficient fresh name generation relying on sets.	Pierre-Marie Pédrot	2017-09-28
\| \|_\|_\|/ / / / / / / / / / / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	The old algorithm was relying on list membership, which is O(n). This was nefarious for terms with many binders. We use instead sets in O(log n).
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| *	[stm] Remove unused "Proof using" data in `Sync` tags.	Emilio Jesus Gallego Arias	2017-09-27
\| \|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|/ \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	This was not used anywhere; it looks like dead code from some previous attempt. `get_hint_ctx` looks also very very suspicious.
\| \| \| \| \| \| \| \| \| \| \| \| \| \| *	Browser userscript to turn BZ#XXXX occurences into links.	Gaëtan Gilbert	2017-09-27
\| \|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|/ \|/\| \| \| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| \| \| \| \| \| \| \| \| *	Avoid looping when searching for CoqProject.	Maxime Dénès	2017-09-27
\| \|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|/ \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	This could happen with paths on Windows, or even relative paths on all OSs. Fixes #5730: CoqIDE becomes unresponsive on file open.
* \| \| \| \| \| \| \| \| \| \| \| \|	Merge PR #688: Binding universe constraints in Definition/Inductive/etc...	Maxime Dénès	2017-09-26
\|\ \ \ \ \ \ \ \ \ \ \ \ \
\| \| \| \| \| \| \| \| \| \| \| \| \| *	look for Obligation num or Next Obligation to start proof	Paul Steckler	2017-09-26
\| \|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|/ \|/\| \| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| \| \| \| \| \| \| \| *	Properly display the "only" prefix for selectors (bug #5760).	Guillaume Melquiond	2017-09-26
\| \|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|/ \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	This commit also fixes range selectors being incorrectly displayed.
\| \| \| \| \| \| \| \| \| \| \| *	Fixing a little parsing bug with level 90 introduced in 3e70ea9c.	Hugo Herbelin	2017-09-25
\| \| \| \| \| \| \| \| \| \| \|/ \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Unfortunately, some manual synchronization is needed between the constr parser and the table of constr/pattern levels. We do this synchronization which was missing in the commit moving "x -> y" to a user-level notation.
* \| \| \| \| \| \| \| \| \| \|	Merge PR #1085: Fix BZ#5755 (incorrect treatment of let-ins in parameters of ↵	Maxime Dénès	2017-09-25
\|\ \ \ \ \ \ \ \ \ \ \ \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	inductive types)
* \ \ \ \ \ \ \ \ \ \ \	Merge PR #1083: Fixing bug in building _rect scheme for inductive types with ↵	Maxime Dénès	2017-09-25
\|\ \ \ \ \ \ \ \ \ \ \ \ \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	let-ins and non-recursively uniform parameters
* \ \ \ \ \ \ \ \ \ \ \ \	Merge PR #1079: Avoid generated names for html pages of the reference manual ↵	Maxime Dénès	2017-09-25
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	(bug #4742).
* \ \ \ \ \ \ \ \ \ \ \ \ \	Merge PR #1068: Fixing #5749 (bug in fold_constr_with_binders introduced in ↵	Maxime Dénès	2017-09-25
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	4e70791).
* \ \ \ \ \ \ \ \ \ \ \ \ \ \	Merge PR #1057: Reporting locations in error messages about notation formats.	Maxime Dénès	2017-09-25
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \	Merge PR #1060: An optimization of tactic constructor	Maxime Dénès	2017-09-25
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \	Merge PR #1075: Re-enable checker error messages	Maxime Dénès	2017-09-25
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \| \|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|/ \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| \| \| * \| \| \| \| \| \| \| \| \|	Discharge.ml: cosmetic renaming of some variables.	Hugo Herbelin	2017-09-23
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	The point is to emphasize stronglier when we are talking about contexts or about arguments.
\| \| \| \| \| \| \| * \| \| \| \| \| \| \| \| \|	Fixing #5755 (discharging of inductive types not correct with let-ins).	Hugo Herbelin	2017-09-23
\| \|_\|_\|_\|_\|_\|/ / / / / / / / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	The number of effective parameters was used where the number of declarations in the signature of parameters should have been used.
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| *	After testing it in live, writing metas using an ?INTERNAL#42 style is ugly.	Hugo Herbelin	2017-09-23
\| \|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|/ \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Printing metas still happens relatively often. From the user point of view, no need to know that it is different from an evar, so the notation ?M42 as it was before is much lighter. As for developers looking for debugging information, they will easily suspect that it is internally a meta because of the "M". This reverts "Proposing meta names more distinguishable from evar names than ?M42." (dc5b8f1793c6f7104f0b4762d9887be255709ead).