| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2017-08-31 | Merge PR #989: Prevent overallocation in Array.map_to_list and remove custom ↵ | Maxime Dénès | |
| implementation from Detyping. | |||
| 2017-08-29 | Merge PR #773: [flags] Remove XML output flag. | Maxime Dénès | |
| 2017-08-22 | Prevent overallocation in Array.map_to_list and remove custom implementation ↵ | Guillaume Melquiond | |
| from Detyping. | |||
| 2017-08-17 | Merge PR #490: A possible fix for #5391 (command line tools do not accept ↵ | Maxime Dénès | |
| trailing / and \ on windows) | |||
| 2017-08-16 | Merge PR #864: Some cleanups after cumulativity for inductive types | Maxime Dénès | |
| 2017-08-15 | Removing trailing "/" and "\" in directory names only on win32. | Hugo Herbelin | |
| This refines e234f3ef. By the way, note that e234f3ef fixed #5391 (command line tools do not accept trailing "/" - or "\" - in windows). | |||
| 2017-08-01 | [flags] Remove XML output flag. | Emilio Jesus Gallego Arias | |
| This is a second try at removing the hooks for the legacy xml export system which can't currently be tested. It is also not included in the API, so it should either be included in it or this PR be applied. | |||
| 2017-07-31 | Change the option for cumulativity | Amin Timany | |
| 2017-07-31 | Merge PR #761: deprecate Pp.std_ppcmds type and promote Pp.t instead | Maxime Dénès | |
| 2017-07-27 | deprecate Pp.std_ppcmds type alias | Matej Košík | |
| 2017-07-26 | Merge PR #902: Only perform profile initialization and printing when the ↵ | Maxime Dénès | |
| flag is set. | |||
| 2017-07-21 | Adding a V8.7 compatibility version number. | Hugo Herbelin | |
| 2017-07-21 | PMP sold us a Timeout on Windows with 1s resolution. Trying to improve it. | Maxime Dénès | |
| 2017-07-20 | coq_makefile: use System.exists_dir for better portability | Enrico Tassi | |
| 2017-07-20 | Windows: Sys.is_dir "foo/" always says no (so we strip trailing slash) | Enrico Tassi | |
| 2017-07-20 | Also a less intrusive Profile.init_profile. | Hugo Herbelin | |
| Calling it only when there is something to profile, or when profiling is explicitly required with the profile flags, so that profiling in plugins is possible. | |||
| 2017-07-20 | A less intrusive Profile.close_profile. | Hugo Herbelin | |
| No need to call Gc functions nor Unix timing functions when there is nothing to report. Moreover, PMP observed problems with these functions in the debugger. PMP also reported that Gc.minor takes some noticeable time, so no need to trigger some when unneeded. | |||
| 2017-07-20 | Merge PR #898: [pp] Fix bugs 5651 [incorrect thunk in pretty printer] | Maxime Dénès | |
| 2017-07-20 | Merge PR #869: Enforce alternating separators in typeclass debug output | Maxime Dénès | |
| 2017-07-19 | [pp] Fix bugs 5651 [incorrect thunk in pretty printer] | Emilio Jesus Gallego Arias | |
| Fix bug introduced by a Haskell programmer. | |||
| 2017-07-17 | Merge PR #862: Adding support for bindings tags to explicit prefix/suffix ↵ | Maxime Dénès | |
| rather than colors | |||
| 2017-07-12 | format pairs of items for pr_depth to get alternating separators | Paul Steckler | |
| eval thunks once in prlist_sep_lastsep, make code clearer add typeclass debug output test | |||
| 2017-07-08 | Adding support for bindings tags to explicit prefix/suffix rather than colors. | Hugo Herbelin | |
| This is usable for no-color terminal. For instance, a typical application in mind is the Coq-generate names marker which can be rendered with a color if the interface supports it and a prefix "~" if the interface does not support colors. | |||
| 2017-07-05 | use Int.equal instead of polymorphic = | Paul Steckler | |
| 2017-07-04 | Merge branch 'v8.6' | Pierre-Marie Pédrot | |
| 2017-07-04 | Bump year in headers. | Pierre-Marie Pédrot | |
| 2017-06-23 | Fix bug 5392: Warnings defined in plugins are considered unknown | Maxime Dénès | |
| The status of a warning can now be set before the warning is declared (typically by a plugin). However, I had to remove the "unknown warning" warning. | |||
| 2017-06-19 | Merge PR#613: Cumulativity for inductive types | Maxime Dénès | |
| 2017-06-19 | Fix typo in comment. | Maxime Dénès | |
| 2017-06-16 | Fix bugs and add an option for cumulativity | Amin Timany | |
| 2017-06-15 | Merge PR#375: Deprecation | Maxime Dénès | |
| 2017-06-14 | Merge PR#739: completing a sentence in a comment | Maxime Dénès | |
| 2017-06-14 | Remove support for Coq 8.4. | Guillaume Melquiond | |
| 2017-06-14 | Remove support for Coq 8.3. | Guillaume Melquiond | |
| 2017-06-14 | Remove support for Coq 8.2. | Guillaume Melquiond | |
| 2017-06-14 | Add a version to be used when parsing compatibility notations mentioning old ↵ | Guillaume Melquiond | |
| versions. | |||
| 2017-06-12 | Add support for "-bypass-API" argument of "coq_makefile" | Matej Košík | |
| Plugin-writers can now use: -bypass-API parameter with "coq_makefile". The effect of that is that instead of -I API the plugin will be compiled with: -I config" -I dev -I lib -I kernel -I library -I engine -I pretyping -I interp -I parsing -I proofs -I tactics -I toplevel -I printing -I intf -I grammar -I ide -I stm -I vernac | |||
| 2017-06-07 | completing a sentence in a comment | Matej Košík | |
| 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 | 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-06-01 | [emacs] [toplevel] Make emacs flag local to the toplevel. | Emilio Jesus Gallego Arias | |
| We remove the emacs-specific printing code from the core of Coq, now `-emacs` is a printing flag controlled by the toplevel. | |||
| 2017-06-01 | Bump year in headers. | Maxime Dénès | |
| 2017-05-30 | Merge PR#356: Making management of installation directories more structured, ↵ | Maxime Dénès | |
| more uniform | |||
| 2017-05-30 | Merge PR#692: Fail on deprecated warning even for Ocaml > 4.02.3 | Maxime Dénès | |
| 2017-05-29 | Relying on computation done in Envars to discover the installation directories. | Hugo Herbelin | |
| This allows to share the test for possible relocalisation done in envars.ml. | |||
| 2017-05-29 | Generalizing to docdir and datadir the test for a relocated installation. | Hugo Herbelin | |
| Also standardizing the choice of the default datadir (I don't see why we should add by default both /usr/local/share/coq and /usr/share/coq when we know that the installation is in only one of them). Open question: test for possible relocation of the installed coq should be done on raw dirname of the executable or on the standardization of this name wrt symbolic links? | |||
| 2017-05-29 | Exporting the suffixes needed to build coqlib, docdir, etc. | Hugo Herbelin | |
| This allows to centralize in the configuration file the description of the 3 possible installation layouts (dispatched over directories shared by multiple application as in unix, self-contained style like in windows, local non-installation as with option -local). Also supporting relocalisation when -prefix or -libdir and co is given. | |||
| 2017-05-29 | Using Coq_config.local rather than None to tell that Coq_config.coqlib is local. | Hugo Herbelin | |
| This goes towards an approach where a local layout can be seen as an installed layout. | |||
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |