aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2016-09-01Short documentation, filling TODO's in evd.mli.Hugo Herbelin
2016-09-01Moving log of "TacReduce"/"reduce" to Tactics.reduce so that internalHugo Herbelin
calls are logged too. Using appropriate printer for reparsability of the output.
2016-08-31Fix Bug #5005 : micromega tactics is now robust to failure of 'abstract'.Frédéric Besson
If 'abstract' fails e.g. if there are existentials. The tactic runs an abstract-free alternative.
2016-08-30Fix bug #5051: Large outputs are garbled.Pierre-Marie Pédrot
Instead of relying on the current position of the cursor, we rather use a dedicated mark in the message view.
2016-08-30Fixing output test-suite after warning for inner Requires.Pierre-Marie Pédrot
2016-08-30Fix bug #4893: not_evar: unexpected failure in 8.5pl1.Pierre-Marie Pédrot
2016-08-30plugin micromega : nra also handles non-linear rational arithmetic over Q ↵Frédéric Besson
(Fixed #4985) Lqa.v defines the tactics lra and nra working over Q. Lra.v defines the tactics lra and nra working over R.
2016-08-30Fix bug #3920: eapply masks an hypothesis name.Pierre-Marie Pédrot
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.
2016-08-30Emit a warning on Require inside a module.Maxime Dénès
2016-08-30Fix #4941 - ~/.coqrc file confusing locationsMaxime Dénès
2016-08-30Missing .PHONY targets.Pierre-Marie Pédrot
2016-08-29Fix bug #4421: Messages dialog in Coqide resets.Pierre-Marie Pédrot
2016-08-29CoqIDE preserves unknown preferences.Pierre-Marie Pédrot
This allows a smoother transition between various versions of CoqIDE, by not erasing options which are unknown at the present time.
2016-08-29Fix tagging of notations.Pierre-Marie Pédrot
We only tag the non-whitespace substrings, rather than the whole terminal token.
2016-08-29Fix inefficiency in CoqIDE display of tagged text.Pierre-Marie Pédrot
The helper code in LablGTK is algorithmically slow, so that we rather reimplement it as a small helper function.
2016-08-29Send Dependency feedback only if file not already loaded.Maxime Dénès
2016-08-28Fix bug #4750: Change format of inconsistent assumptions message.Pierre-Marie Pédrot
We now print the file responsible for the incompatibility in require error messages.
2016-08-28Fix bug #4764: Syntactic notation externalization breaks.Pierre-Marie Pédrot
2016-08-27Support qualified identifiers in Show Match (bug #5050).Guillaume Melquiond
2016-08-25FIX: Coq versionMatej Kosik
2016-08-25Do not export an internal function in Namegen.Pierre-Marie Pédrot
2016-08-24Properly compute types for assumed section variables (bug #5035).Guillaume Melquiond
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
2016-08-24Merge PR #260: "Fix bug 4842 (Time prints in multiple lines)" into v8.6Pierre-Marie Pédrot
2016-08-24Merge PR #258: "Fix newline issues" into v8.6Pierre-Marie Pédrot
2016-08-23Fix bug #4914: LtacProf printout has too many newlines.Pierre-Marie Pédrot
2016-08-23Arguments: give / after last ! error detection fixedEnrico Tassi
2016-08-23fix get_host_port error message (#4724)Enrico Tassi
2016-08-23update Proof General URLPaul Steckler
2016-08-23Fix bug #4904: [Import] does not load intermediately unqualified names of ↵Pierre-Marie Pédrot
aliases.
2016-08-22Fast path for set operations.Pierre-Marie Pédrot
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.
2016-08-22Merge remote-tracking branch 'github/pr/261' into v8.6Maxime Dénès
Was PR#261: Use a better data structure for VM compilation of free vars.
2016-08-22Use a better data structure for VM compilation of free vars.Pierre-Marie Pédrot
This fixes #3450 and probably provides a huge speed-up to many instances.
2016-08-22Pushing error backtrace in unification reraise.Pierre-Marie Pédrot
2016-08-21Documenting "Set Structural Injection".Hugo Herbelin
2016-08-21Do not recompute the whole evar naming environment in GProd intepretation.Pierre-Marie Pédrot
2016-08-21Short path for Pretyping.ltac_interp_name_env.Pierre-Marie Pédrot
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!
2016-08-21Merge branch 'v8.5' into v8.6Pierre-Marie Pédrot
2016-08-20More standard naming for the Imparg.with_implicits function.Pierre-Marie Pédrot
2016-08-20Fixing a bug in the presence of let-in while inferring the return clause.Hugo Herbelin
2016-08-20Fixing an anomaly in printing a unification error message.Hugo Herbelin
2016-08-19Test file for bug #4187.Pierre-Marie Pédrot
2016-08-19Fix performance bug: do not compute implicits of abstracted lemmas.Pierre-Marie Pédrot
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.
2016-08-19Removing dead code in Impargs.Pierre-Marie Pédrot
2016-08-19[pp] Fix bug 4842 (Time prints in multiple lines)Emilio Jesus Gallego Arias
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.
2016-08-19Merge remote-tracking branch 'origin/pr/246' into v8.6Matthieu Sozeau
2016-08-19Moving Taccoerce to ltac/ folder.Pierre-Marie Pédrot
This was an overlook. There was no reason to let it in the tactics/ folder, as is was semantically part of the Ltac implementation.
2016-08-19Remove extraneous dot in error message (bug #4832).Guillaume Melquiond
2016-08-19Fix anomaly on user-inputted projection name (bug #5029).Guillaume Melquiond
2016-08-19[pp] Fix newline issues.Emilio Jesus Gallego Arias
This is a followup to 91ee24b4a7843793a84950379277d92992ba1651 , where we got a few cases wrong wrt to newline endings. Thanks to @herbelin for pointing it out. This doesn't yet fix https://coq.inria.fr/bugs/show_bug.cgi?id=4842
2016-08-18Merge remote-tracking branch 'github/bug4978' into v8.6Matthieu Sozeau
generated by cgit v1.2.3 (git 2.25.1) at 2026-10-11 16:34:19 +0000