aboutsummaryrefslogtreecommitdiffhomepage
path: root/lib
Commit message (Collapse)AuthorAge
* Merge PR #761: deprecate Pp.std_ppcmds type and promote Pp.t insteadGravatar Maxime Dénès2017-07-31
|\
| * deprecate Pp.std_ppcmds type aliasGravatar Matej Košík2017-07-27
| |
* | Merge PR #902: Only perform profile initialization and printing when the ↵Gravatar Maxime Dénès2017-07-26
|\ \ | | | | | | | | | flag is set.
* | | Adding a V8.7 compatibility version number.Gravatar Hugo Herbelin2017-07-21
| |/ |/|
* | PMP sold us a Timeout on Windows with 1s resolution. Trying to improve it.Gravatar Maxime Dénès2017-07-21
| |
* | coq_makefile: use System.exists_dir for better portabilityGravatar Enrico Tassi2017-07-20
| |
* | Windows: Sys.is_dir "foo/" always says no (so we strip trailing slash)Gravatar Enrico Tassi2017-07-20
| |
| * Also a less intrusive Profile.init_profile.Gravatar Hugo Herbelin2017-07-20
| | | | | | | | | | | | 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.
| * A less intrusive Profile.close_profile.Gravatar Hugo Herbelin2017-07-20
| | | | | | | | | | | | | | | | | | 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.
* | Merge PR #898: [pp] Fix bugs 5651 [incorrect thunk in pretty printer]Gravatar Maxime Dénès2017-07-20
|\ \
* \ \ Merge PR #869: Enforce alternating separators in typeclass debug outputGravatar Maxime Dénès2017-07-20
|\ \ \ | |_|/ |/| |
| | * [pp] Fix bugs 5651 [incorrect thunk in pretty printer]Gravatar Emilio Jesus Gallego Arias2017-07-19
| |/ |/| | | | | Fix bug introduced by a Haskell programmer.
* | Merge PR #862: Adding support for bindings tags to explicit prefix/suffix ↵Gravatar Maxime Dénès2017-07-17
|\ \ | | | | | | | | | rather than colors
| | * format pairs of items for pr_depth to get alternating separatorsGravatar Paul Steckler2017-07-12
| | | | | | | | | | | | | | | eval thunks once in prlist_sep_lastsep, make code clearer add typeclass debug output test
| * | Adding support for bindings tags to explicit prefix/suffix rather than colors.Gravatar Hugo Herbelin2017-07-08
| |/ | | | | | | | | | | | | | | 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.
* / use Int.equal instead of polymorphic =Gravatar Paul Steckler2017-07-05
|/
* Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2017-07-04
|\
* | Bump year in headers.Gravatar Pierre-Marie Pédrot2017-07-04
| |
| * Fix bug 5392: Warnings defined in plugins are considered unknownGravatar Maxime Dénès2017-06-23
| | | | | | | | | | | | 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.
* | Merge PR#613: Cumulativity for inductive typesGravatar Maxime Dénès2017-06-19
|\ \
* | | Fix typo in comment.Gravatar Maxime Dénès2017-06-19
| | |
| * | Fix bugs and add an option for cumulativityGravatar Amin Timany2017-06-16
|/ /
* | Merge PR#375: DeprecationGravatar Maxime Dénès2017-06-15
|\ \
* \ \ Merge PR#739: completing a sentence in a commentGravatar Maxime Dénès2017-06-14
|\ \ \
| | * | Remove support for Coq 8.4.Gravatar Guillaume Melquiond2017-06-14
| | | |
| | * | Remove support for Coq 8.3.Gravatar Guillaume Melquiond2017-06-14
| | | |
| | * | Remove support for Coq 8.2.Gravatar Guillaume Melquiond2017-06-14
| | | |
| | * | Add a version to be used when parsing compatibility notations mentioning old ↵Gravatar Guillaume Melquiond2017-06-14
| |/ / |/| | | | | | | | versions.
* | | Add support for "-bypass-API" argument of "coq_makefile"Gravatar Matej Košík2017-06-12
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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
| * | completing a sentence in a commentGravatar Matej Košík2017-06-07
| | |
* | | Put all plugins behind an "API".Gravatar Matej Kosik2017-06-07
|/ /
* | Merge PR#728: A few typos.Gravatar Maxime Dénès2017-06-06
|\ \
| * | A few typos.Gravatar Hugo Herbelin2017-06-04
| | |
* | | Drop '.' from CErrors.anomaly, insert it in argsGravatar Jason Gross2017-06-02
|/ / | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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 ```
* | [emacs] [toplevel] Make emacs flag local to the toplevel.Gravatar Emilio Jesus Gallego Arias2017-06-01
| | | | | | | | | | We remove the emacs-specific printing code from the core of Coq, now `-emacs` is a printing flag controlled by the toplevel.
| * Bump year in headers.Gravatar Maxime Dénès2017-06-01
| |
* | Merge PR#356: Making management of installation directories more structured, ↵Gravatar Maxime Dénès2017-05-30
|\ \ | | | | | | | | | more uniform
* \ \ Merge PR#692: Fail on deprecated warning even for Ocaml > 4.02.3Gravatar Maxime Dénès2017-05-30
|\ \ \
| | * | Relying on computation done in Envars to discover the installation directories.Gravatar Hugo Herbelin2017-05-29
| | | | | | | | | | | | | | | | This allows to share the test for possible relocalisation done in envars.ml.
| | * | Generalizing to docdir and datadir the test for a relocated installation.Gravatar Hugo Herbelin2017-05-29
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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?
| | * | Exporting the suffixes needed to build coqlib, docdir, etc.Gravatar Hugo Herbelin2017-05-29
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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.
| | * | Using Coq_config.local rather than None to tell that Coq_config.coqlib is local.Gravatar Hugo Herbelin2017-05-29
| | | | | | | | | | | | | | | | | | | | This goes towards an approach where a local layout can be seen as an installed layout.
| | * | Configuration: always giving a value to configdir and datadir.Gravatar Hugo Herbelin2017-05-29
| | | | | | | | | | | | | | | | | | | | | | | | | | | | They were not used for looking for coqide files in the situation when the effective installation path happens to be exactly the installation path proposed by default, while relevant files were however (possibly) installed in these directories.
| | * | Dead code (xdg_config_dirs).Gravatar Hugo Herbelin2017-05-29
| | | |
| * | | Fail on deprecated warning even for Ocaml > 4.02.3Gravatar Gaëtan Gilbert2017-05-28
| |/ / | | | | | | | | | | | | | | | | | | | | | Deprecations which can't be fixed in 4.02.3 are locally wrapped with [@@@ocaml.warning "-3"]. The only ones encountered are - capitalize to capitalize_ascii and variants. Changing to ascii would break coqdoc -latin1 and maybe other things though. - external "noalloc" to external [@@noalloc]
* / / [cleanup] Unify all calls to the error function.Gravatar Emilio Jesus Gallego Arias2017-05-27
|/ / | | | | | | | | | | | | | | | | | | | | | | | | 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.
* | Merge PR#666: romega revisited : no more normalization trace, cleaned-up ↵Gravatar Maxime Dénès2017-05-26
|\ \ | | | | | | | | | resolution trace
* \ \ Merge PR#655: Extra functions exported in EConstrGravatar Maxime Dénès2017-05-26
|\ \ \
* \ \ \ Merge PR#645: [stm] Tweak debug options.Gravatar Maxime Dénès2017-05-25
|\ \ \ \
* \ \ \ \ Merge PR#406: coq makefile2Gravatar Maxime Dénès2017-05-25
|\ \ \ \ \
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-26 14:12:31 +0000