| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2017-04-04 | closing bug file for #4306 | Julien Forest | |
| 2017-04-04 | end of correction of bug 4306 | Julien Forest | |
| 2017-04-04 | Bad correction in previous commit | Julien Forest | |
| 2017-04-04 | Solving first problem in bug #4306. TO DO : solve the let in problem | Julien Forest | |
| 2017-04-04 | bug file for 4306 | Julien Forest | |
| 2017-04-04 | Adding tests for chained abstract tactics. | Pierre-Marie Pédrot | |
| 2017-04-04 | Fix substitution of abstracted lemmas. | Pierre-Marie Pédrot | |
| Instead of browsing the term as many times as there are abstracted constants, we replace the constants in one pass. We have to be a bit careful to replace the right variables though, in case there are chained abstracts. This is much faster. This solves the second part of bug #5382: Huge case analysis fails in coq8.5.x. | |||
| 2017-04-04 | Merge PR#502: [pp] Add anomaly header to error messages. | Maxime Dénès | |
| 2017-04-04 | Merge branch 'trunk' into pr379 | Maxime Dénès | |
| 2017-04-04 | Merge PR#535: Fix #5435: [Eval native_compute in] raises anomaly. | Maxime Dénès | |
| 2017-04-04 | Test file for #5435: [Eval native_compute in] raises anomaly. | Maxime Dénès | |
| 2017-04-04 | Fix bug #5435: [Eval native_compute in] raises anomaly. | Maxime Dénès | |
| Was introduced by 4f041384cb27f0d2. Unsoundness seems miraculously avoided by a safeguard I put in nativecode.ml. But other kernel changes in this commit should probably be reviewed carefully. | |||
| 2017-04-03 | Merge branch 'v8.6' into trunk | Maxime Dénès | |
| 2017-04-03 | Merge PR#533: Instances should obey universe binders even when defined by ↵ | Maxime Dénès | |
| tactics. | |||
| 2017-04-03 | Fix loading of ocamldebug printers. | Pierre-Marie Pédrot | |
| 2017-04-03 | Instances should obey universe binders even when defined by tactics. | Gaetan Gilbert | |
| 2017-04-03 | Merge PR#417: No cast surgery in let in | Maxime Dénès | |
| 2017-04-03 | Add test file for #4957. | Maxime Dénès | |
| Bug #4957 was "unify cannot directly unify universes with evars, but can do so indirectly". | |||
| 2017-04-02 | Fix higher-order pattern variables not being printed as "@?" (bug #5431). | Guillaume Melquiond | |
| 2017-04-02 | Fix documentation typo (bug #5433). | Guillaume Melquiond | |
| 2017-04-02 | Simplify some proofs. | Guillaume Melquiond | |
| This commit does not modify the signature of the involved modules, only the opaque proof terms. One has to wonder how proofs can bitrot so much that several occurrences of "replace 4 with 4" start appearing. | |||
| 2017-04-01 | Restore a fast path in EConstr instance normalization. | Pierre-Marie Pédrot | |
| 2017-04-01 | Using delayed universe instances in EConstr. | Pierre-Marie Pédrot | |
| The transition has been done a bit brutally. I think we can still save a lot of useless normalizations here and there by providing the right API in EConstr. Nonetheless, this is a first step. | |||
| 2017-04-01 | Declaring ltac plugin, so that static linking works. | Hugo Herbelin | |
| 2017-04-01 | Actually exporting delayed universes in the EConstr implementation. | Pierre-Marie Pédrot | |
| For now we only normalize sorts, and we leave instances for the next commit. | |||
| 2017-03-31 | Make the Constr.kind_of_term type parametric in sorts and universes. | Pierre-Marie Pédrot | |
| 2017-03-31 | Ensuring proper cast invariants in EConstr.kind. | Pierre-Marie Pédrot | |
| The kernel does fishy things with casts, such that ensuring there are no two consecutive VMcast or NATIVEcast in terms. We enforce this in EConstr view as well. | |||
| 2017-03-31 | Revert "Specially crafted EConstr.kind to be more efficient." | Pierre-Marie Pédrot | |
| This reverts commit b5f07be9fdcd41fdaf73503e5214e766bf6a303b. The performance difference was not conclusive enough to pay for the code ugliness. | |||
| 2017-03-30 | Specially crafted EConstr.kind to be more efficient. | Pierre-Marie Pédrot | |
| We do one step of loop unrolling, limit the number of allocations and mark the function as inline. | |||
| 2017-03-30 | Merge branch 'v8.6' into trunk | Maxime Dénès | |
| 2017-03-30 | Merge PR#463: Run non-tactic comands without resilient_command | Maxime Dénès | |
| 2017-03-30 | Fix ring_simplify sometimes producing R0 and R1 instead of 0%R and 1%R. | Guillaume Melquiond | |
| 2017-03-30 | Merge PR#469: Added take to VectorDef | Maxime Dénès | |
| 2017-03-30 | Added take to VectorDef. | George Stelle | |
| Added a function that takes the first [p] elements of a vector, and a few lemmas proving some of its properties. | |||
| 2017-03-30 | Merge PR#511: [stm] Remove some obsolete vernacs/classification. | Maxime Dénès | |
| 2017-03-29 | Merge PR#522: [coqide] Protect against size_allocate race in proofview. | Maxime Dénès | |
| 2017-03-29 | Merge branch 'v8.6' into trunk | Maxime Dénès | |
| 2017-03-29 | Merge PR#514: [travis] Backport from trunk: VST | Maxime Dénès | |
| 2017-03-29 | Merge PR#506: [nit] Fix a couple incorrect uses of msg_error. | Maxime Dénès | |
| 2017-03-29 | Merge PR#521: Do so that "About" tells if a reference is a coercion. | Maxime Dénès | |
| 2017-03-29 | Merge PR#525: [ide] Fix typo in pp serialization. | Maxime Dénès | |
| 2017-03-29 | Merge branch 'trunk' into pr379 | Maxime Dénès | |
| 2017-03-29 | Fix call to broken unsafe_type_of in apply tactic. | Maxime Dénès | |
| This broke the build of iris-coq in the EConstr branch. Each time you use unsafe_type_of, I loose a night of sleep, so please stop. | |||
| 2017-03-29 | Run non-tactic comands without resilient_command | Tej Chajed | |
| 2017-03-29 | [ide] Fix typo in pp serialization. | Emilio Jesus Gallego Arias | |
| 2017-03-28 | Revert to incorrect heuristic in apply. | Maxime Dénès | |
| Was breaking e.g. fiat-crypto. | |||
| 2017-03-28 | Fixing missing PropFacts.v in Logic/vo.itarget. | Hugo Herbelin | |
| This is while waiting for a possible different solution, if ever such a different solution is adopted, since the coq.inria.fr/library has currently a broken link and someone rightly complained about it. | |||
| 2017-03-28 | [readme] Add badges for Travis and Gitter. | Emilio Jesus Gallego Arias | |
| 2017-03-28 | [coqide] Protect against size_allocate race in proofview. | Emilio Jesus Gallego Arias | |
| To handle dynamic printing in CoqIDE we listen to the `size_allocate` signal , [see more details in 6885a398229918865378ea24f07d93d2bcdd2802] However, we must be careful to protect against scrollbar creation: it is possible for the `size_allocate` handler to change the size when inserting text (due to scrollbars), thus we may enter in an infinite loop. Our fix is to check if the width has really changed, as done in `Wg_MessageView`. This fixes the problem noted by @herbelin in https://coq.inria.fr/bugs/show_bug.cgi?id=5417 | |||
| 2017-03-27 | Do so that "About" tells if a reference is a coercion. | Hugo Herbelin | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |