| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2017-05-23 | Merge PR#646: Revised behavior on ill-formed identifiers | Maxime Dénès | |
| 2017-05-23 | Merge PR#518: Faster universe unification | Maxime Dénès | |
| 2017-05-20 | Revised behavior on ill-formed identifiers. | Hugo Herbelin | |
| Namely: Replacing (currently deactivated) warning on illegal ident by an error in strict mode and nothing in soft mode. | |||
| 2017-05-11 | Merge PR#572: Replacing costly merges in UGraph. | Maxime Dénès | |
| 2017-05-03 | Merge PR#602: Fix more warnings | Maxime Dénès | |
| 2017-05-03 | Merge PR#411: Mention template polymorphism in the documentation. | Maxime Dénès | |
| 2017-05-02 | Remove dead code in native compiler. | Maxime Dénès | |
| 2017-05-02 | Merge PR#582: Fix warnings | Maxime Dénès | |
| 2017-05-01 | More consistent writing of de Bruijn. | Théo Zimmermann | |
| 2017-05-01 | Fix for bug 5507. Mispelt de Bruijn. | Théo Zimmermann | |
| 2017-04-28 | Merge PR#531: Fixing bug #5420 and many similar bugs due to the presence of ↵ | Maxime Dénès | |
| let-ins | |||
| 2017-04-27 | Fix 4.04 warnings | Gaetan Gilbert | |
| 2017-04-27 | Remove some unused values and types | Gaetan Gilbert | |
| 2017-04-27 | Fix omitted labels in function calls | Gaetan Gilbert | |
| 2017-04-27 | Locally disable some warnings. | Gaetan Gilbert | |
| 2017-04-27 | Fast path when checking equality of universe levels in UState. | Pierre-Marie Pédrot | |
| We export the relevant level equality function in UGraph which is way faster than checking that each one is smaller than the other as universes. | |||
| 2017-04-20 | COMMENT: Pre_env.env | Matej Kosik | |
| 2017-04-20 | correcting a typo in a comment | Matej Kosik | |
| 2017-04-20 | correcting comments in the "Context" module | Matej Kosik | |
| 2017-04-20 | simplifying "Environ.push_named" function | Matej Kosik | |
| 2017-04-20 | refactoring "Names.DirPath.is_empty" function | Matej Kosik | |
| 2017-04-20 | refactoring "Names.DirPath.compare" function | Matej Kosik | |
| 2017-04-20 | refactoring "Names.DirPath.equal" function | Matej Kosik | |
| 2017-04-18 | Replacing costly merges in UGraph. | Pierre-Marie Pédrot | |
| 2017-04-15 | Merge branch 'v8.6' into trunk | Maxime Dénès | |
| 2017-04-12 | Merge PR#441: Port Toplevel to the Stm API | Maxime Dénès | |
| 2017-04-12 | [stm] Remove edit_id. | Emilio Jesus Gallego Arias | |
| We remove `edit_id` from the STM. In PIDE they serve a different purpose, however in Coq they were of limited utility and required many special cases all around the code. Indeed, parsing is not an asynchronous operation in Coq, thus having feedback about parsing didn't make much sense. All clients indeed ignore such feedback and handle parsing in a synchronous way. XML protocol clients are unaffected, they rely on the instead on the Fail value. This commit supersedes PR#203. | |||
| 2017-04-11 | Merge PR#549: Fast path in weak head reduction of applied atoms. | Maxime Dénès | |
| 2017-04-11 | Update various comments to use "template polymorphism" | Gaetan Gilbert | |
| Also remove obvious comments. | |||
| 2017-04-11 | Merge PR#537: Efficient side-effect abstraction | Maxime Dénès | |
| 2017-04-09 | Documenting how the recursive indices of a fixpoint are computed. | Hugo Herbelin | |
| Also documenting how the implicit arguments by position are computed. | |||
| 2017-04-08 | Fast path in weak head reduction of applied atoms. | Pierre-Marie Pédrot | |
| Instead of calling the whole reduction machirery, we check before reducing that a term is an applied atom, i.e. inductive, constructor, evar or meta. In that case, the abstract machine acts as the identity but needs to destruct and reconstruct the whole term, which can be very costly. This fixes part of bug #5421: vm_compute is very slow at doing nothing, where recomputation of the type of a big inductive was incredibly expensive. | |||
| 2017-04-07 | Merge branch 'master' into econstr | Pierre-Marie Pédrot | |
| 2017-04-07 | Merge PR#519: Faster side effects | Maxime Dénès | |
| 2017-04-07 | Inline the only use of hcons_j in Term_typing. | Pierre-Marie Pédrot | |
| 2017-04-06 | Documenting the fact terms are only hashconsed outside of a section. | Pierre-Marie Pédrot | |
| 2017-04-05 | Merge PR#434: Optimizing array mapping in the kernel. | Maxime Dénès | |
| 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 | 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-03-31 | Make the Constr.kind_of_term type parametric in sorts and universes. | Pierre-Marie Pédrot | |
| 2017-03-27 | More efficient check in validity of side-effects. | Pierre-Marie Pédrot | |
| We don't need to look for the size of the whole list to find whether we can extract a suffix from it, as we can do it in one go instead. This slowness was observable in abstract-heavy code. | |||
| 2017-03-27 | Adding the size of the opaquetab in its representation. | Pierre-Marie Pédrot | |
| This turned out to be costly in proofs with many abstracted lemmas, as an important part of the time was passed in the computation of the size of the opaquetab. | |||
| 2017-03-27 | Fix hashconsing of terms in the kernel. | Pierre-Marie Pédrot | |
| In one case, the hashconsed type of a judgement was not used anywhere else. In another case, the Opaqueproof module was rehashconsing terms that had already gone through a hashconsing phase. Indeed, most OpaqueDef constructor applications actually called it beforehand, so that the one performed in Opaqueproof was most often useless. The only case where this was not true was at section closing time, so that we tweak the Cooking.cook_constant to perform hashconsing for us. | |||
| 2017-03-24 | Merge branch 'trunk' into pr379 | Maxime Dénès | |
| 2017-03-24 | Merge branch 'v8.6' into trunk | Maxime Dénès | |
| 2017-03-23 | Documenting the API of side-effects. | Pierre-Marie Pédrot | |
| 2017-03-23 | Using a dedicated datastructure for side effect ordering. | Pierre-Marie Pédrot | |
| We were doing fishy things in the Term_typing file, where side-effects were not considered in the right uniquization order because of the uniq_seff_rev function. It probably did not matter after a9b76df because effects were (mostly) uniquize upfront, but this is not clear because of the use of the transparente API in the module. Now everything has to go through the opaque API, so that a proper dependence order is ensured. | |||
| 2017-03-23 | Making the side_effects type opaque. | Pierre-Marie Pédrot | |
| We move it from Entries to Term_typing and export the few functions needed to manipulate it in this module. | |||
| 2017-03-23 | Merge branch 'v8.6' into trunk | Maxime Dénès | |
| 2017-03-22 | Merge branch 'v8.6' | Pierre-Marie Pédrot | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |