aboutsummaryrefslogtreecommitdiffhomepage
path: root/library
Commit message (Collapse)AuthorAge
* Use Pp.quote in string options.Gravatar Maxime Dénès2016-12-19
|
* Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-11-18
|\
| * 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).
| * Put string between quotes when printing an option value.Gravatar Maxime Dénès2016-11-02
| | | | | | | | This is a better (more generic) fix to #5061 than my e8b9ee76.
* | Moving Universes to the engine/ folder.Gravatar Pierre-Marie Pédrot2016-10-30
| | | | | | | | | | | | Before this patch, this module was a member of the library folder, which had little to do with its actual use. A tiny part relative to global registering of universe names has been effectively moved to the Global module.
* | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-10-29
|\|
| * Merge remote-tracking branch 'github/pr/337' into v8.6Gravatar Maxime Dénès2016-10-28
| |\ | | | | | | | | | Was PR#337: Fix arguments
| | * Add missing dot to impargs error message.Gravatar Maxime Dénès2016-10-27
| | |
| | * Proper fix for #3753 (anomaly with implicit arguments and renamings)Gravatar Maxime Dénès2016-10-27
| | | | | | | | | | | | | | | | | | | | | | | | Instead of circumventing the problem on the caller's side, as was done in Arguments, we simply avoid failing as there was no real reason for this anomaly to be triggered. If the list of renamings is shorter than the one of implicits, we simply interpret the remaining arguments as not renamed.
| | * Complete overhaul of the Arguments vernacular.Gravatar Maxime Dénès2016-10-27
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | The main point of this change is to fix #3035: Avoiding trailing arguments in the Arguments command, and related issues occurring in HoTT for instance. When the "assert" flag is not specified, we now accept prefixes of the list of arguments. The semantics of _ w.r.t. to renaming has changed. Previously, it meant "restore the original name inferred from the type". Now it means "don't change the current name". The syntax of arguments is now restricted. Modifiers like /, ! and scopes are allowed only in the first arguments list. We also add *a lot* of missing checks on input values and fix various bugs. Note that this code is still way too complex for what it does, due to the complexity of the implicit arguments, reduction behaviors and renaming APIs.
* | | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-10-24
|\| |
| * | Cleanup code according to comments.Gravatar Matthieu Sozeau2016-10-20
| | |
| * | Fix minimization to be insensitive to redundant arcs.Gravatar Matthieu Sozeau2016-10-20
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | The new algorithm produces different sets of arcs than in 8.5, hence existing developments may fail to pass now because they relied on the (correct but more approximate) result of minimization in 8.5 which wasn't insensitive. The algorithm works bottom-up on the (well-founded) graph to find lower levels that an upper level can be minimized to. We filter said lower levels according to the lower sets of the other levels we consider. If they appear in any of them then we don't need their constraints. Does not seem to have a huge impact on performance in HoTT, but this should be evaluated further. Adapt test-suite files accordingly.
| * | Merge branch 'bug5036' into v8.6Gravatar Matthieu Sozeau2016-10-20
| |\ \ | | |/ | |/|
| | * Fix bug #5036 autorewrite, sections and universesGravatar Matthieu Sozeau2016-10-20
| | | | | | | | | | | | | | | | | | Universe context not properly declared. Improve API and code in declare.ml to allow declaration of universe contexts, used by declaration of universes and constraints (separately).
* | | COMMENT: was added to "Nameops.increment_suffix".Gravatar Matej Kosik2016-10-19
| | |
* | | CLEANUP: rename "Nameops.lift_subscript" to "Nameops.increment_subscript".Gravatar Matej Kosik2016-10-19
| | | | | | | | | | | | | | | | | | | | | The word "increment" is more appropriate in this case than "lifting". The world "lifting", in computer science, usually denotes something else: https://en.wikipedia.org/wiki/Lambda_lifting
* | | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-10-05
|\| |
| * | Fix a bug of Mltop.declare_cache_object.Gravatar Pierre-Marie Pédrot2016-10-05
| | | | | | | | | | | | | | | | | | | | | Objects registered through the callback functions were pushed on the libstack before the ML-MODULE object itself, leading to anomalies when the corresponding object was assuming that the ML module was properly defined in any other Coq module requiring the Declare ML command.
| * | Changing the separator for appended string options to comma.Gravatar Maxime Dénès2016-10-04
| | | | | | | | | | | | | | | | | | This is a bit ad-hoc, but looks better for warnings since there is a command-line flag accepting the same values, so comma will lead to fewer parsing issues than space.
* | | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-10-02
|\ \ \
| | * | Allow appending to string options.Gravatar Guillaume Melquiond2016-10-01
| |/ / | | | | | | | | | | | | | | | | | | Whether an option should be set or appended to is stored as a 2-value flag next to the new content. This commit also cleans the code by declaring a single object for each persistent option rather than three different ones (one per locality).
| * | Merge remote-tracking branch 'github/pr/299' into v8.6Gravatar Maxime Dénès2016-09-30
| |\ \ | | | | | | | | | | | | | | | | Was PR#299: Fix bug #4869, allow Prop, Set, and level names in constraints.
| * | | Fix bug #5036 autorewrite, sections and universesGravatar Matthieu Sozeau2016-09-29
| | |/ | |/| | | | | | | | | | | | | Universe context not properly declared. Improve API and code in declare.ml to allow declaration of universe contexts, used by declaration of universes and constraints (separately).
| | * Fix bug #4869, allow Prop, Set, and level names in constraints.Gravatar Matthieu Sozeau2016-09-29
| |/
* | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-09-27
|\|
| * Fix bug #5090: Effect of -Q depends on coqtop's current directory.Gravatar Pierre-Marie Pédrot2016-09-25
| | | | | | | | | | | | | | This bug was seemingly introduced on purpose by commit 9c5ea63 in 2001. It seems that the original motivation was to deactivate a warning when overriding the default loadpath binding of the current directory, but in the end it made it non-overridable.
* | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-09-23
|\|
* | Revert "Merge remote-tracking branch 'github/pr/283' into trunk"Gravatar Maxime Dénès2016-09-22
| | | | | | | | | | | | | | | | | | I hadn't realized that this PR uses OCaml's 4.03 inlined records feature. I will advocate again for a switch to the latest OCaml stable version, but meanwhile, let's revert. Sorry for the noise. This reverts commit 3c47248abc27aa9c64120db30dcb0d7bf945bc70, reversing changes made to ceb68d1d643ac65f500e0201f61e73cf22e6e2fb.
* | Rename Decl_kinds.binding_kind into Decls_kind.implicit_status.Gravatar Maxime Dénès2016-09-20
| | | | | | | | | | | | | | | | | | The new name makes it more obvious what is meant here by "kind". We leave Decl_kinds.binding_kind as a deprecated alias for plugin compatibility. We also replace bool with implicit_status in a few places in the codebase.
* | Stylistic improvements in intf/decl_kinds.mli.Gravatar Maxime Dénès2016-09-20
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | We get rid of tuples containing booleans (typically for universe polymorphism) by replacing them with records. The previously common idom: if pi2 kind (* polymorphic *) then ... else ... becomes: if kind.polymorphic then ... else ... To make the construction and destruction of these records lightweight, the labels of boolean arguments for universe polymorphism are now usually also called "polymorphic".
| * Remove dead code in library/lib.ml.Gravatar Maxime Dénès2016-09-20
| |
* | Merge PR #244.Gravatar Pierre-Marie Pédrot2016-09-08
|\ \
* \ \ Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-09-07
|\ \ \ | | |/ | |/|
| * | A proposal to unify the messages given by Test and Print Options (#5062).Gravatar Hugo Herbelin2016-09-06
| | |
| * | Summary: simpler API for process-local storageGravatar Enrico Tassi2016-09-05
| | |
* | | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-09-02
|\| |
| * | Emit a warning on Require inside a module.Gravatar Maxime Dénès2016-08-30
| | |
* | | CLEANUP: switching from "right-to-left" to "left-to-right" function ↵Gravatar Matej Kosik2016-08-30
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | composition operator. Short story: This pull-request: (1) removes the definition of the "right-to-left" function composition operator (2) adds the definition of the "left-to-right" function composition operator (3) rewrites the code relying on "right-to-left" function composition to rely on "left-to-right" function composition operator instead. Long story: In mathematics, function composition is traditionally denoted with ∘ operator. Ocaml standard library does not provide analogous operator under any name. Batteries Included provides provides two alternatives: _ % _ and _ %> _ The first operator one corresponds to the classical ∘ operator routinely used in mathematics. I.e.: (f4 % f3 % f2 % f1) x ≜ (f4 ∘ f3 ∘ f2 ∘ f1) x We can call it "right-to-left" composition because: - the function we write as first (f4) will be called as last - and the function write as last (f1) will be called as first. The meaning of the second operator is this: (f1 %> f2 %> f3 %> f4) x ≜ (f4 ∘ f3 ∘ f2 ∘ f1) x We can call it "left-to-right" composition because: - the function we write as first (f1) will be called first - and the function we write as last (f4) will be called last That is, the functions are written in the same order in which we write and read them. I think that it makes sense to prefer the "left-to-right" variant because it enables us to write functions in the same order in which they will be actually called and it thus better fits our culture (we read/write from left to right).
* | | CLEANUP: using |> operator more consistentlyGravatar Matej Kosik2016-08-30
| | |
| * | Send Dependency feedback only if file not already loaded.Gravatar Maxime Dénès2016-08-29
| | |
| * | Fix bug #4750: Change format of inconsistent assumptions message.Gravatar Pierre-Marie Pédrot2016-08-28
| | | | | | | | | | | | | | | We now print the file responsible for the incompatibility in require error messages.
* | | CLEANUP: minor readability improvementsGravatar Matej Kosik2016-08-24
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | mainly concerning referring to "Context.{Rel,Named}.get_{id,value,type}" functions. If multiple modules define a function with a same name, e.g.: Context.{Rel,Named}.get_type those calls were prefixed with a corresponding prefix to make sure that it is obvious which function is being called.
* | | CLEANUP: removing superfluous (module) qualifiersGravatar Matej Kosik2016-08-24
| | |
* | | Changing the definition of the "Lib.variable.info" type to enable us to do ↵Gravatar Matej Kosik2016-08-24
|/ / | | | | | | more cleanups
* | More standard naming for the Imparg.with_implicits function.Gravatar Pierre-Marie Pédrot2016-08-20
| |
* | Removing dead code in Impargs.Gravatar Pierre-Marie Pédrot2016-08-19
| |
| * Make the user_err header an optional parameter.Gravatar Emilio Jesus Gallego Arias2016-08-19
| | | | | | | | Suggested by @ppedrot
| * Remove errorlabstrm in favor of user_errGravatar Emilio Jesus Gallego Arias2016-08-19
| | | | | | | | | | | | | | As noted by @ppedrot, the first is redundant. The patch is basically a renaming. We didn't make the component optional yet, but this could happen in a future patch.
| * Unify location handling of error functions.Gravatar Emilio Jesus Gallego Arias2016-08-19
|/ | | | | | | | | | | | | | In some cases prior to this patch, there were two cases for the same error function, one taking a location, the other not. We unify them by using an option parameter, in the line with recent changes in warnings and feedback. This implies a bit of clean up in some places, but more importantly, is the preparation for subsequent patches making `Loc.location` opaque, change that could be use to improve modularity and allow a more functional implementation strategy --- for example --- of the beautifier.
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-25 06:02:54 +0000