aboutsummaryrefslogtreecommitdiffhomepage
path: root/lib
Commit message (Collapse)AuthorAge
* [pp] Prepare for serialization, remove opaque glue.Gravatar Emilio Jesus Gallego Arias2017-03-21
| | | | | We also remove flushing operations `msg_with`, now the flushing responsibility belong to the owner of the formatter.
* [pp] Remove `Pp.stras`.Gravatar Emilio Jesus Gallego Arias2017-03-21
| | | | Mostly unused, we ought to limit spacing in the boxes themselves.
* [pp] Replace `Pp.Tag` by `Ppstyle.tag` = `string list`Gravatar Emilio Jesus Gallego Arias2017-03-21
| | | | | | | | This is what has always been used, so it doesn't represent a functional change. This is just a preliminary patch, but many more possibilities could be done wrt tags.
* Merge PR#134: Enable `-safe-string`Gravatar Maxime Dénès2017-03-21
|\
| * [safe-string] lib/miscelaneaGravatar Emilio Jesus Gallego Arias2017-03-14
| | | | | | | | No functional change.js
| * [safe-string] lib/cUnixGravatar Emilio Jesus Gallego Arias2017-03-14
| | | | | | | | No functional change.
| * [safe_string] lib/cThreadGravatar Emilio Jesus Gallego Arias2017-03-14
| | | | | | | | No functional changes.
* | [future] Remove unused parameter greedy.Gravatar Emilio Jesus Gallego Arias2017-03-14
|/ | | | It was always set to `greedy:true`.
* Merge PR#189: Remove tabulation support from pretty-printing.Gravatar Maxime Dénès2017-02-20
|\
* | [unicode] Address comments in PR#314.Gravatar Emilio Jesus Gallego Arias2017-02-15
| |
* | [safe-string] Use `String.init` to build string.Gravatar Emilio Jesus Gallego Arias2017-02-14
| |
* | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2017-02-01
|\ \
* \ \ Merge PR#355: Remove unused feedback_content: GoalsGravatar Maxime Dénès2017-01-30
|\ \ \
| | * \ Merge PR#383: fix #5244: set printing width ignored when given enough spaceGravatar Maxime Dénès2017-01-24
| | |\ \
* | | \ \ Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2017-01-19
|\ \ \ \ \ | | |/ / / | |/| | |
| * | | | Fix race condition in STM DAG generation (in debug mode).Gravatar Maxime Dénès2017-01-13
| | | | | | | | | | | | | | | | | | | | The same file name for .dot graphs could be used by concurrent processes.
| * | | | Fix broken .aux machinery.Gravatar Guillaume Melquiond2017-01-13
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Coq expects aux_file_name_for to give the aux file corresponding to the input file whichever its Coq-related extension, be it .v or .vo or .vio. Commit 3e6fa1c broke this contract when fixing bug #5183. As a consequence, depending on the execution path, Coq would try to save or load from either .foo.aux or .foo.vo.aux or .foo.vio.aux. This commit reverts 3e6fa1c and fixes bug #5183 much earlier in the call chain by not initializing hints when the input file does not end with .v. This also restores 8.5 behavior with respect to aux file naming.
* | | | | Avoid using the deprecated Scanf.fscanf function.Gravatar Maxime Dénès2017-01-09
| | | | |
* | | | | Merge remote-tracking branch 'github/pr/351' into trunkGravatar Maxime Dénès2016-12-19
|\ \ \ \ \ | | | | | | | | | | | | | | | | | | Was PR#351: Complete a truncated comment
* \ \ \ \ \ Merge remote-tracking branch 'github/pr/363' into trunkGravatar Maxime Dénès2016-12-19
|\ \ \ \ \ \ | | | | | | | | | | | | | | | | | | | | | Was PR#363: lib/Unicodetable: Update.
| | | | | * | [pp] Set printing width for richpp formatter (bug #5244)Gravatar Emilio Jesus Gallego Arias2016-12-04
| | | | |/ / | | | |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Richpp output depends on printing width, thus its internal formatter should be seeded with the proper width value. While we are at it, we increase the default buffer size to a more sensible value.
* | | | | | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-11-30
|\ \ \ \ \ \ | | |_|/ / / | |/| | | |
| * | | | | Fix #5183 - Two CoqIDE crash errorsGravatar Maxime Dénès2016-11-30
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | When opening a file without extension, an uncaught exception was occurring. Note that this fix is not complete, since the "Compile Buffer" command still fails. This is because of a limitation of coqc which appends the ".v" extension to its argument even if it already existed (and even if it doesn't exist with the extension!).
| * | | | | Fix some documentation typos.Gravatar Guillaume Melquiond2016-11-24
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Note: "dependant" does exist, but it is a noun and it means a person that is somehow financially dependent on someone else.
* | | | | | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-11-18
|\| | | | |
| | * | | | lib/Unicodetable: Update. This code has been generated from the latestGravatar Yann Régis-Gianas2016-11-16
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Unicode tables using UUCD, an OCaml library to parse the official Unicode tables.
| * | | | | Fix bug in warnings: -w foo was silent when foo did not exist.Gravatar Maxime Dénès2016-11-14
| | | | | |
| | | | * | Remove unused feedback_content: GoalsGravatar CJ Bell2016-11-10
| |_|_|/ / |/| | | |
| | | * | Complete a truncated commentGravatar Arnaud Spiwack2016-11-08
| |_|/ / |/| | | | | | | | | | | | | | | Introduce by myself, I'm afraid, in #308. Noticed by PMP during the review, but I forgot to fix it before merge.
| * | | Removing a special treatment for empty lines in comments.Gravatar Hugo Herbelin2016-11-05
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This made the whole pp code complicated only for the purpose of the beautifier, while it is not clear when this was useful. Removing the code for simplicity, not excluding to later address beautifier issues when they show up.
| * | | Fix #4837: ./configure -local makes coqdep issue many warningsGravatar Maxime Dénès2016-11-04
| | | | | | | | | | | | | | | | | | | | | | | | We simply remove the warnings about paths mixing Win32 and Unix separators, since that situation does not seem problematic (c.f. discussion on the bug tracker).
| * | | Remove an OCaml 4.02 construct.Gravatar Maxime Dénès2016-11-03
| | | | | | | | | | | | | | | | | | | | This was not detected by running coq-contribs, so it probably means that we are not testing with the right version of OCaml.
| * | | Fix various shortcomings of the warnings infrastructure.Gravatar Maxime Dénès2016-11-02
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | - The flags are now interpreted from left to right, without any other precedence rule. The previous one did not make much sense in interactive mode. - Set Warnings and Set Warnings Append are now synonyms, and have the "append" semantics, which is the most natural one for warnings. - Warnings on unknown warnings are now printed only once (previously the would be repeated on further calls to Set Warnings, sections closing, module requiring...). - Warning status strings are normalized, so that e.g. "+foo,-foo" is reduced to "-foo" (if foo exists, "" otherwise).
* | | | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-10-29
|\| | |
| * | | Merge remote-tracking branch 'github/pr/319' into v8.6Gravatar Maxime Dénès2016-10-28
| |\ \ \ | | | | | | | | | | | | | | | Was PR#319: More error tagging, try to fix bug 5135
| * | | | STM: make ~valid state id non optional from APIsGravatar Enrico Tassi2016-10-26
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | It used to be Stateid.initial by default. That is indeed a valid state id but very likely not the very best one (that would be the tip of the document).
* | | | | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-10-24
|\| | | |
| * | | | Error Resiliency: more conservative default (only curly braces)Gravatar Enrico Tassi2016-10-19
| | | | |
| | * | | [pp] Try to properly tag error messages in cError.Gravatar Emilio Jesus Gallego Arias2016-10-18
| |/ / / | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | In order to get proper coloring, we must tag the headers of error messages in `CError`. This should fix bug https://coq.inria.fr/bugs/show_bug.cgi?id=5135 However, note that this could interact badly with the richpp printing used by the IDE. At this level, we have no clue which tag we'd like to apply, as we know (and shouldn't) nothing about the top level backend. Thus, for now I've selected the console printer, hoping that the `Richpp` won't crash the IDE.
* | | | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-10-18
|\| | |
| * | | Stopping warning on unrecognized unicode character in notation (fixing #5136).Gravatar Hugo Herbelin2016-10-17
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | The warning was pointless since the notation was accepted and parsed anyway. We now treat unrecognized unicode characters like ordinary undefined tokens (e.g. "#" in a bare Coq). For instance, "aₚ", or ".ₚ", or "?ₚ" now fail with "Undefined token" rather than "Unsupported Unicode character".
| * | | [toplevel] Remove duplicate beautify flags.Gravatar Emilio Jesus Gallego Arias2016-10-17
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Given the current style in flags.mli no reason to have a function. A deeper question is why a global flag is needed, in particular the use in `interp/constrextern.ml` seems strange, the condition in the lexer should be looked at and I'm not sure about `printing/`.
* | | | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-10-17
|\| | |
| * | | Merge PR #224 into v8.6Gravatar Pierre-Marie Pédrot2016-10-12
| |\ \ \
* | | | | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-10-12
|\| | | |
| * | | | Merge branch 'v8.5' into v8.6Gravatar Pierre-Marie Pédrot2016-10-12
| |\ \ \ \
| | * | | | Fix #4416: - Incorrect "Error: Incorrect number of goals"Gravatar Arnaud Spiwack2016-10-10
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | In `Ftactic` the number of results could desynchronise with the number of goals when some goals were solved by side effect in a different branch of a `DISPATCH`. See [coq-bugs#4416](https://coq.inria.fr/bugs/show_bug.cgi?id=4416).
| * | | | | Moving Pp.comments to CLexer so that Pp is purer (no more side-effectGravatar Hugo Herbelin2016-10-09
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | done by the Ppcmd_comment token) and so that lexing/parsing side-effects are collected at the same place, i.e. in CLexer.
* | | | | | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-10-02
|\| | | | |
| | | * | | [pp] Remove duplicate color logger.Gravatar Emilio Jesus Gallego Arias2016-09-30
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | We use the same printing path for color and mono terminal output, thus removing the duplicate printers which avoids problems as they don't have to be kept in sync anymore. We tag unconditionally but set the `pp_tag` tagger properly. This removes IO from `Ppstyle` with IMO is the right thing to do. Test suite passes.
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-28 18:41:47 +0000