| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2017-06-14 | Merge PR#738: [kernel] Improve proof using message, fixes bugzilla #3613 | Maxime Dénès | |
| 2017-06-14 | Merge PR#448: Do not recompute twice the whnf of terms in conversion. | Maxime Dénès | |
| 2017-06-13 | Merge PR#714: Print feature Proof-of-Concept (episode 2) | Maxime Dénès | |
| 2017-06-10 | Remove (useless) aliases from the API. | Matej Košík | |
| 2017-06-07 | [kernel] Improve proof using message, fixes bugzilla #3613 | Emilio Jesus Gallego Arias | |
| 2017-06-07 | Put all plugins behind an "API". | Matej Kosik | |
| 2017-06-06 | Merge PR#728: A few typos. | Maxime Dénès | |
| 2017-06-04 | Added support for a side effect on constants in reduction functions. | Thomas Sibut-Pinote | |
| This exports two functions: - declare_reduction_effect: to declare a hook to be applied when some constant are visited during the execution of some reduction functions (primarily cbv, but also cbn, simpl, hnf, ...). - set_reduction_effect: to declare a constant on which a given effect hook should be called. Developed jointly by Thomas Sibut-Pinote and Hugo Herbelin. Added support for printing effect in functions of tacred.ml. | |||
| 2017-06-04 | A few typos. | Hugo Herbelin | |
| 2017-06-02 | Drop '.' from CErrors.anomaly, insert it in args | Jason Gross | |
| As per https://github.com/coq/coq/pull/716#issuecomment-305140839 Partially using ```bash git grep --name-only 'anomaly\s*\(~label:"[^"]*"\s*\)\?\(Pp.\)\?(\(\(Pp.\)\?str\)\?\s*".*[^\.!]")' | xargs sed s'/\(anomaly\s*\(~label:"[^"]*"\s*\)\?\(Pp.\)\?(\(\(Pp.\)\?str\)\?\s*".*\s*[^\.! ]\)\s*")/\1.")/g' -i ``` and ```bash git grep --name-only ' !"' | xargs sed s'/ !"/!"/g' -i ``` The rest were manually edited by looking at the results of ```bash git grep anomaly | grep '\.ml' | grep -v 'anomaly\s*\(~label:"[^"]*"\s*\)\?\(Pp\.\)\?(\(\(Pp.\)\?str\)\?\s*".*\(\.\|!\)")' | grep 'anomaly\($\|[^_]\)' | less ``` | |||
| 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 | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |