| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2016-09-02 | Fast path in whd_evar. | Pierre-Marie Pédrot | |
| Before computing the whd_evar-form of the arguments of an evar, we first check that it is indeed defined. | |||
| 2016-09-02 | Silence the CAMLP5 warnings on command line. | Pierre-Marie Pédrot | |
| They were mostly useless, and people complained about it. Not that because there is no API to make CAMLP4 silent, a CAMLP4-based Coq will still spit out its share of noisy warnings. | |||
| 2016-09-02 | Remove useless debug code. | Guillaume Melquiond | |
| 2016-09-02 | Merge branch 'v8.5' into v8.6 | Pierre-Marie Pédrot | |
| 2016-09-01 | Fix test-suite after Frédéric's 6231f07b2. | Maxime Dénès | |
| 2016-09-01 | Fixed Bug #5003 : more careful generalisation of dependent terms. | Frédéric Besson | |
| 2016-09-01 | More efficient data structure to check if a native file is loaded. | Maxime Dénès | |
| Spotted by PMP. | |||
| 2016-09-01 | Notation_ops.subst_glob_vars: substituting also in evar kind for | Hugo Herbelin | |
| consistency of the use of names. | |||
| 2016-09-01 | 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 | |
| (It was reducing also in hypotheses.) | |||
| 2016-09-01 | Moving log of "TacReduce"/"reduce" to Tactics.reduce so that internal | Hugo Herbelin | |
| calls are logged too. Using appropriate printer for reparsability of the output. | |||
| 2016-09-01 | Fixing name of internal refine ("simple refine"). | Hugo Herbelin | |
| 2016-08-31 | Fix 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-31 | Fix bug #5043: [Admitted] lemmas pick up section variables. | Pierre-Marie Pédrot | |
| 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. | |||
| 2016-08-30 | Fix 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-30 | 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 | |
| (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-30 | Fix 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-30 | 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 | |
| Fix done with Enrico. | |||
| 2016-08-30 | Missing .PHONY targets. | Pierre-Marie Pédrot | |
| 2016-08-30 | micromega cache files are now hidden files (cf #4156) | Frédéric Besson | |
| csdp.cache -> .csdp.cache lia.cache -> .lia.cache nlia.cache -> .nia.cache | |||
| 2016-08-30 | Setting an unknown option now always a warning. Fixes #4947. | Maxime Dénès | |
| 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. | |||
| 2016-08-29 | Fix bug #4421: Messages dialog in Coqide resets. | Pierre-Marie Pédrot | |
| 2016-08-29 | CoqIDE 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-29 | Fix tagging of notations. | Pierre-Marie Pédrot | |
| We only tag the non-whitespace substrings, rather than the whole terminal token. | |||
| 2016-08-29 | Fix 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-29 | Send Dependency feedback only if file not already loaded. | Maxime Dénès | |
| 2016-08-28 | Fix 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-28 | Fix bug #4764: Syntactic notation externalization breaks. | Pierre-Marie Pédrot | |
| 2016-08-27 | Support qualified identifiers in Show Match (bug #5050). | Guillaume Melquiond | |
| 2016-08-25 | FIX: Coq version | Matej Kosik | |
| 2016-08-25 | Do not export an internal function in Namegen. | Pierre-Marie Pédrot | |
| 2016-08-24 | Properly 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-24 | 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-23 | 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 | |
| aliases. | |||
| 2016-08-22 | Fast 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-22 | Merge remote-tracking branch 'github/pr/261' into v8.6 | Maxime Dénès | |
| Was PR#261: Use a better data structure for VM compilation of free vars. | |||
| 2016-08-22 | Use 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-22 | Pushing error backtrace in unification reraise. | Pierre-Marie Pédrot | |
| 2016-08-21 | 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 | |
| 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! | |||
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |