| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2016-08-11 | CLEANUP: removing a call of "Context.Rel.Declaration.to_tuple" function | Matej Kosik | |
| 2016-08-11 | CLEANUP: removing a call of "Context.Rel.Declaration.to_tuple" function | Matej Kosik | |
| 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 | remove checker/Makefile | Pierre Letouzey | |
| This historical Makefile was used during the development of coqcheck, but was unused since then : the checker is built via Coq's main Makefile. So let's remove this one to avoid any risk of confusion. | |||
| 2016-07-26 | No more dev/printers.cma | Pierre Letouzey | |
| This file was only used during ocamldebug sessions (in the dev/db script). It was containing a large subset of the core cma files, up to the printing functions. There were a few notable exceptions, for instance no kernel/vm.cmo to avoid loading dllcoqrun.so in ocamldebug. But printers.cma was troublesome to maintain : almost each time an ML file was added/removed/renamed in the core of Coq, dev/printers.mllib had to be edited, in addition to the directory-specific .mllib (kernel/kernel.mllib and co). So I propose here to kill this file, and put instead in dev/db several "load_printer" of the core cma files. For that to work, we need to compile kernel/kernel.cma with the right -dllib and -dllpath options, but that shouldn't hurt (on the contrary). We also source now the camlpX cma in dev/db, via a new generated file dev/camlp4.dbg containing a load_printer of either gramlib.cma or camp4lib.cma. If one doesn't want to perform the whole "source db" at the start of an ocamldebug session, then the former "load_printer printers.cma" could be replaced by: source core.dbg load_printer top_printers.cmo See for instance the minimal dev/base_db. | |||
| 2016-07-26 | Makefile.build: minor simplification | Pierre Letouzey | |
| 2016-07-26 | Merge branch 'v8.6' into trunk | Pierre Letouzey | |
| 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.6' | Pierre-Marie Pédrot | |
| 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. | |||
| 2016-07-19 | Notations with multiple recursive binders: fixing use of alpha-conversion. | Hugo Herbelin | |
| 2016-07-19 | Fixing missing parentheses in printing of patterns in binders. | Hugo Herbelin | |
| (In agreement with Daniel.) | |||
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |