coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
...
* \|	Short documentation, filling TODO's in evd.mli.	Hugo Herbelin	2016-09-01
\| \|
\| *	Fixing call to "lazy beta iota" in "refine" (restoring v8.4 behavior).	Hugo Herbelin	2016-09-01
\| \| \| \| \| \| \| \|	(It was reducing also in hypotheses.)
* \|	Moving log of "TacReduce"/"reduce" to Tactics.reduce so that internal	Hugo Herbelin	2016-09-01
\| \| \| \| \| \| \| \| \| \|	calls are logged too. Using appropriate printer for reparsability of the output.
\| *	Fixing name of internal refine ("simple refine").	Hugo Herbelin	2016-09-01
\| \|
* \|	Fix Bug #5005 : micromega tactics is now robust to failure of 'abstract'.	Frédéric Besson	2016-08-31
\| \| \| \| \| \| \| \|	If 'abstract' fails e.g. if there are existentials. The tactic runs an abstract-free alternative.
\| *	Fix bug #5043: [Admitted] lemmas pick up section variables.	Pierre-Marie Pédrot	2016-08-31
\| \| \| \| \| \| \| \| \| \| \| \|	We add a flag Keep Admitted Variables that allows to recover the legacy v8.4 behaviour of admitted lemmas. The statement of such lemmas did not depend on the current context variables.
* \|	Fix bug #5051: Large outputs are garbled.	Pierre-Marie Pédrot	2016-08-30
\| \| \| \| \| \| \| \| \| \|	Instead of relying on the current position of the cursor, we rather use a dedicated mark in the message view.
* \|	Fixing output test-suite after warning for inner Requires.	Pierre-Marie Pédrot	2016-08-30
\| \|
* \|	Fix bug #4893: not_evar: unexpected failure in 8.5pl1.	Pierre-Marie Pédrot	2016-08-30
\| \|
* \|	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.
* \|	Fix bug #3920: eapply masks an hypothesis name.	Pierre-Marie Pédrot	2016-08-30
\| \| \| \| \| \| \| \| \| \| \| \|	The problem came from the fact that the legacy beta-reduction occurring after a rewrite was wrongly applied to the side-conditions of the rewriting step. We restrict it to the correct goal in this patch.
* \|	Emit a warning on Require inside a module.	Maxime Dénès	2016-08-30
\| \|
* \|	Fix #4941 - ~/.coqrc file confusing locations	Maxime Dénès	2016-08-30
\| \|
\| *	Fix #4871 - interrupting par:abstract kills coqtop	Maxime Dénès	2016-08-30
\| \| \| \| \| \| \| \|	Fix done with Enrico.
* \|	Missing .PHONY targets.	Pierre-Marie Pédrot	2016-08-30
\| \|
\| *	micromega cache files are now hidden files (cf #4156)	Frédéric Besson	2016-08-30
\| \| \| \| \| \| \| \| \| \| \| \|	csdp.cache -> .csdp.cache lia.cache -> .lia.cache nlia.cache -> .nia.cache
\| *	Setting an unknown option now always a warning. Fixes #4947.	Maxime Dénès	2016-08-30
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Previously, setting an unknown option was an error or a warning, depending on the type of the option. We make it always a warning, for forward compatibility. This was already fixed in 8.6.
* \|	Fix bug #4421: Messages dialog in Coqide resets.	Pierre-Marie Pédrot	2016-08-29
\| \|
* \|	CoqIDE preserves unknown preferences.	Pierre-Marie Pédrot	2016-08-29
\| \| \| \| \| \| \| \| \| \|	This allows a smoother transition between various versions of CoqIDE, by not erasing options which are unknown at the present time.
* \|	Fix tagging of notations.	Pierre-Marie Pédrot	2016-08-29
\| \| \| \| \| \| \| \|	We only tag the non-whitespace substrings, rather than the whole terminal token.
* \|	Fix inefficiency in CoqIDE display of tagged text.	Pierre-Marie Pédrot	2016-08-29
\| \| \| \| \| \| \| \| \| \|	The helper code in LablGTK is algorithmically slow, so that we rather reimplement it as a small helper function.
* \|	Send Dependency feedback only if file not already loaded.	Maxime Dénès	2016-08-29
\| \|
* \|	Fix bug #4750: Change format of inconsistent assumptions message.	Pierre-Marie Pédrot	2016-08-28
\| \| \| \| \| \| \| \| \| \|	We now print the file responsible for the incompatibility in require error messages.
* \|	Fix bug #4764: Syntactic notation externalization breaks.	Pierre-Marie Pédrot	2016-08-28
\| \|
* \|	Support qualified identifiers in Show Match (bug #5050).	Guillaume Melquiond	2016-08-27
\| \|
* \|	FIX: Coq version	Matej Kosik	2016-08-25
\| \|
* \|	Do not export an internal function in Namegen.	Pierre-Marie Pédrot	2016-08-25
\| \|
* \|	Properly compute types for assumed section variables (bug #5035).	Guillaume Melquiond	2016-08-24
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	This bug was introduced by commit 34ef02fac1110673ae74c41c185c228ff7876de2 Author: Matej Kosik <m4tej.kosik@gmail.com> Date: Fri Jan 29 10:13:12 2016 +0100 CLEANUP: Context.{Rel,Named}.Declaration.t
* \|	Merge PR #260: "Fix bug 4842 (Time prints in multiple lines)" into v8.6	Pierre-Marie Pédrot	2016-08-24
\|\ \
* \ \	Merge PR #258: "Fix newline issues" into v8.6	Pierre-Marie Pédrot	2016-08-24
\|\ \ \
* \| \| \|	Fix bug #4914: LtacProf printout has too many newlines.	Pierre-Marie Pédrot	2016-08-23
\| \| \| \|
* \| \| \|	Arguments: give / after last ! error detection fixed	Enrico Tassi	2016-08-23
\| \| \| \|
* \| \| \|	fix get_host_port error message (#4724)	Enrico Tassi	2016-08-23
\| \| \| \|
* \| \| \|	update Proof General URL	Paul Steckler	2016-08-23
\| \| \| \|
* \| \| \|	Fix bug #4904: [Import] does not load intermediately unqualified names of ↵	Pierre-Marie Pédrot	2016-08-23
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	aliases.
* \| \| \|	Fast path for set operations.	Pierre-Marie Pédrot	2016-08-22
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	We consider an approximation of the size of sets before choosing the most appropriate algorithm. This drastically affects some universe-polymorphic code which was doing a lot of set operations on disimilar sizes.
* \| \| \|	Merge remote-tracking branch 'github/pr/261' into v8.6	Maxime Dénès	2016-08-22
\|\ \ \ \ \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Was PR#261: Use a better data structure for VM compilation of free vars.
\| * \| \| \|	Use a better data structure for VM compilation of free vars.	Pierre-Marie Pédrot	2016-08-22
\|/ / / / \| \| \| \| \| \| \| \| \| \| \| \|	This fixes #3450 and probably provides a huge speed-up to many instances.
* \| \| \|	Pushing error backtrace in unification reraise.	Pierre-Marie Pédrot	2016-08-22
\| \| \| \|
* \| \| \|	Documenting "Set Structural Injection".	Hugo Herbelin	2016-08-21
\| \| \| \|
* \| \| \|	Do not recompute the whole evar naming environment in GProd intepretation.	Pierre-Marie Pédrot	2016-08-21
\| \| \| \|
* \| \| \|	Short path for Pretyping.ltac_interp_name_env.	Pierre-Marie Pédrot	2016-08-21
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Instead of recomputing the evar name environment from scratch when it is unchanged, we simply return the original one. This should fix #4964 for good, although I still find the global evar naming mechanism from Pretyping more than messy. Introducing the heuristic allowing to capture variables from Ltac in constr binders is indeed the root of many evils... That is far from being a zero-cost abstraction!
* \| \| \|	Merge branch 'v8.5' into v8.6	Pierre-Marie Pédrot	2016-08-21
\|\ \ \ \ \| \| \|_\|/ \| \|/\| \|
* \| \| \|	More standard naming for the Imparg.with_implicits function.	Pierre-Marie Pédrot	2016-08-20
\| \| \| \|
* \| \| \|	Fixing a bug in the presence of let-in while inferring the return clause.	Hugo Herbelin	2016-08-20
\| \| \| \|
\| * \| \|	Fixing an anomaly in printing a unification error message.	Hugo Herbelin	2016-08-20
\| \| \| \|
* \| \| \|	Test file for bug #4187.	Pierre-Marie Pédrot	2016-08-19
\| \| \| \|
* \| \| \|	Fix performance bug: do not compute implicits of abstracted lemmas.	Pierre-Marie Pédrot	2016-08-19
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	This was showing up in some of Jason's examples, where an abstract had to compute the weak head form of a huge term in order to find the corresponding implicit arguments.
* \| \| \|	Removing dead code in Impargs.	Pierre-Marie Pédrot	2016-08-19
\| \| \| \|
\| \| \| *	[pp] Fix bug 4842 (Time prints in multiple lines)	Emilio Jesus Gallego Arias	2016-08-19
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	This commit proposes a fix for https://coq.inria.fr/bugs/show_bug.cgi?id=4842 The previous feature is a bit complicated to do correctly due to the separation over who has control of the console. Indeed, `-timed` is a command line option of the batch compiler, so we resort to a hack and assume control over the console. I am not very happy with this solution but should do the job. Note that the timing event is still being sent by the standard msg mechanism. A particular point of interest is the duplication of paths between the stm and vernac.