| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2017-05-31 | Creating a module Nameops.Name extending module Names.Name. | Hugo Herbelin | |
| This module collects the functions of Nameops which are about Name.t and somehow standardize or improve their name, resulting in particular from discussions in working group. Note the use of a dedicated exception rather than a failwith for Nameops.Name.out. Drawback of the approach: one needs to open Nameops, or to use long prefix Nameops.Name. | |||
| 2017-05-29 | Merge PR#555: Missing optimization when Kernel Term Sharing is disabled. | Maxime Dénès | |
| 2017-05-27 | [cleanup] Unify all calls to the error function. | Emilio Jesus Gallego Arias | |
| This is the continuation of #244, we now deprecate `CErrors.error`, the single entry point in Coq is `user_err`. The rationale is to allow for easier grepping, and to ease a future cleanup of error messages. In particular, we would like to systematically classify all error messages raised by Coq and be sure they are properly documented. We restore the two functions removed in #244 to improve compatibility, but mark them deprecated. | |||
| 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-12 | Missing optimization when Kernel Term Sharing is disabled. | Pierre-Marie Pédrot | |
| We don't have to perfom in-place updates because we actually know that there is none on the stack. This should speed up UniMath. | |||
| 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 | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |