| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2016-08-17 | Fixing printing in debugger (no global env in debugger). | Hugo Herbelin | |
| 2016-08-17 | A fix to dev/include. | Hugo Herbelin | |
| 2016-08-16 | Removing dead unsafe debugging code in Constrintern. | Pierre-Marie Pédrot | |
| 2016-08-16 | Merge PR #250 into v8.6 | Pierre-Marie Pédrot | |
| 2016-08-16 | Merge PR #237 into v8.6 | Pierre-Marie Pédrot | |
| 2016-08-16 | Merge branch 'v8.5' into v8.6 | Pierre-Marie Pédrot | |
| 2016-08-16 | Efficiently generate the pretyping contexts. | Pierre-Marie Pédrot | |
| We used to recompute all fresh named contexts for evars before this patch in the push_rel_context_to_named_context function. This was incurring a linear penalty and a memory explosion due to the reallocation of many arrays. Now, we rather remember the context between evar creations by sharing it in the pretyping environment. This can be considered as a fix for bug #4964 even though we might do better. | |||
| 2016-08-16 | Merge branch 'pr255' into v8.5 (bug #5015) | Guillaume Melquiond | |
| 2016-08-14 | Fix regression in Coqide's "forward one command" command | Xavier Leroy | |
| In Coqide 8.5pl2, "forward one command" (down arrow) always repositions the insertion point at the end of the phrase being executed, just after the final ".". In Coqide 8.4, the insertion point is not moved if it is after the end of the executed phrase. The insertion point is moved only if it falls behind the phrase being executed. I find the 8.5 behavior to be a regression over the lot more useful 8.4 behavior. This commit restores the 8.4 behavior of "forward one command". | |||
| 2016-08-11 | Do not assume the "TERM" environment variable is always set (bug #5007). | Guillaume Melquiond | |
| 2016-08-11 | Use the "md5" command on OpenBSD (bug #5008). | Guillaume Melquiond | |
| 2016-08-10 | Make code a bit clearer by removing optional argument. | Guillaume Melquiond | |
| 2016-08-10 | Remove unused optional "predicative" argument. | Guillaume Melquiond | |
| 2016-08-10 | Make it a bit more obvious when variables are of type unit. | Guillaume Melquiond | |
| 2016-08-09 | Reduce warning noise when compiling the standard library. | Guillaume Melquiond | |
| 2016-08-09 | Make List.map_filter(_i) tail-recursive. | Guillaume Melquiond | |
| While the performance gain should go unnoticed in most cases, in some degenerate situations, e.g. the evar-stressing test-case of bug #4964, this commit speeds up coq by 10% since most of the time is spent scanning long lists with most of the elements filtered out. Note that this commit also changes the scanning order to front-to-back, which is a bit less surprising (though no code should ever depend on the scanning order). | |||
| 2016-08-07 | Fix #5000: Document the native compiler soundness bug due to Unicode mangling. | Pierre-Marie Pédrot | |
| 2016-08-06 | Using a dedicated kind of substitutions in evar name generation. | Pierre-Marie Pédrot | |
| This saves a quadratic allocation by replacing arrays with maps. | |||
| 2016-08-05 | Using the extended contexts in pretyping. | Pierre-Marie Pédrot | |
| In addition to sharing, we also delay the computation of the environment in a by-need fashion. | |||
| 2016-08-04 | Use sets instead of lists for names to avoid in evar generation. | Pierre-Marie Pédrot | |
| 2016-08-04 | Simplifying code in evar generation. | Pierre-Marie Pédrot | |
| We remove in particular a dubious use of an environment in fresh name generation. The code was using the wrong environment in a function only depending on the rel context which was resetted most of the time. This might change the generated names in extremely rare occurences. | |||
| 2016-08-04 | Exporting the renaming API for evar declaration. | Pierre-Marie Pédrot | |
| 2016-08-04 | Embedding the pretyping environment in a dummy record. | Pierre-Marie Pédrot | |
| 2016-08-04 | Fix documentation typo (bug #4994). | Guillaume Melquiond | |
| 2016-07-29 | Fix bug #4673: regression in setoid_rewrite. | Matthieu Sozeau | |
| Modulo delta for types should be fully transparent. | |||
| 2016-07-29 | Merge remote-tracking branch 'gforge/v8.5' into v8.6 | Matthieu Sozeau | |
| 2016-07-29 | Update CHANGES about #3886 bugfix | Matthieu Sozeau | |
| 2016-07-29 | Fix bug #3886, generation of obligations of fixes | Matthieu Sozeau | |
| This partially reverts c14ccd1b8a3855d4eb369be311d4b36a355e46c1 | |||
| 2016-07-29 | Fix #4769, univ poly and elim schemes in sections | Matthieu Sozeau | |
| 2016-07-29 | COMMENT: moving misplaced comment where it belongs | Matej Kosik | |
| 2016-07-26 | Adding a flag in CoqIDE to configure UNIX/Windows line ending. | Pierre-Marie Pédrot | |
| Fixes both bugs #4924 and #4437. | |||
| 2016-07-26 | restore compatibility with gallium's camlp4 (broken by commit 8e07227c) | Pierre Letouzey | |
| Apparently, in camlp4 (unlike camlp5) : - Something like "[ kwd = IDENT "foobar" -> .... kwd ... ]" produces a kwd of type token instead of string (which sounds reasonable ?). For now, I've replaced kwd by the explicit strings. Not so nice, but works with both camlp4 and camlp5 - A quotation of the form "let obj = ... in bar; baz" is not interpreted in the usual OCaml way, but rather as "(let obj = ... in bar); baz". Let's use instead "let obj = ... in let () = bar in baz", which works fine. | |||
| 2016-07-26 | Update CHANGES about critical bugfix and others | Matthieu Sozeau | |
| 2016-07-26 | Merge branch 'bug4754' into v8.5 | Matthieu Sozeau | |
| 2016-07-26 | Fix bug #4754, allow conversion problems to remain | Matthieu Sozeau | |
| when checking that the rewrite relation is homogeneous in setoid_rewrite. | |||
| 2016-07-26 | Merge remote-tracking branch 'gforge/v8.5' into v8.6 | Matthieu Sozeau | |
| 2016-07-26 | Merge branch 'bug4876' into v8.5 | Matthieu Sozeau | |
| 2016-07-25 | Merge remote-tracking branch 'github/bug4679' into v8.6 | Matthieu Sozeau | |
| 2016-07-25 | Fix bug #4876: critical bug in guard condition checker. | Matthieu Sozeau | |
| 2016-07-21 | Fix bug #4679, weakened setoid_rewrite unification | Matthieu Sozeau | |
| It should use evar instantiations eagerly during unification of the lhs of the lemma, as in 8.4. | |||
| 2016-07-20 | Merge branch 'v8.5' into v8.6 | Pierre-Marie Pédrot | |
| 2016-07-20 | Update CHANGES | Matthieu Sozeau | |
| 2016-07-20 | Fix bug #4780: universe leak in letin_tac | Matthieu Sozeau | |
| 2016-07-20 | Update CHANGES | Matthieu Sozeau | |
| 2016-07-20 | Fix bug #4780: universe leak in letin_tac | Matthieu Sozeau | |
| 2016-07-19 | Allow `STDTIME=foo make` | Jason Gross | |
| This gives better behavior both when including the `coq_makefile` `Makefile` into other `Makefile`s and when setting `STDTIME` through an environment variable. | |||
| 2016-07-19 | Fix Errors.out missing a dot... | Matthieu Sozeau | |
| 2016-07-19 | Complementing previous commit on fixes for printing binding patterns. | Hugo Herbelin | |
| 2016-07-19 | Some extra fixes in printing patterns in binders. | Hugo Herbelin | |
| - typo in notation_ops.ml - factorization of patterns in ppconstr.ml - update of test-suite - printing of cast of a binding pattern if in mode "printing all" The question of whether or not to print the type of a binding pattern by default seems open to me. | |||
| 2016-07-19 | Taking into account binding patterns when agglutinating sequences of binders. | Hugo Herbelin | |
| Supporting accordingly printing of sequences of binders including binding patterns. | |||
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |