aboutsummaryrefslogtreecommitdiffhomepage
path: root/library
Commit message (Collapse)AuthorAge
* Remove unused [open] statementsGravatar Gaetan Gilbert2017-04-27
|
* [flags] Deprecate is_silent/is_verbose in favor of single flag.Gravatar Emilio Jesus Gallego Arias2017-04-21
| | | | | | | | | Today, both modes are controlled by a single flag, however this is a bit misleading as is_silent really means "quiet", that is to say `coqc -q` whereas "verbose" is Coq normal operation. We also restore proper behavior of goal printing in coqtop on quiet mode, thanks to @Matafou for the report.
* Fix a normalization hotspot in computation of constr keys.Gravatar Pierre-Marie Pédrot2017-04-06
| | | | | Getting a key only needs to observe the root of a term. This hotspot was observed in HoTT.
* Merge branch 'trunk' into pr379Gravatar Maxime Dénès2017-04-04
|\
* \ Merge branch 'trunk' into pr379Gravatar Maxime Dénès2017-03-24
|\ \
| | * [nit] Fix a couple incorrect uses of msg_error.Gravatar Emilio Jesus Gallego Arias2017-03-24
| |/
| * Merge PR#390: Updates to the Pretty Printing InfrastructureGravatar Maxime Dénès2017-03-22
| |\
| * \ Merge PR#478: Small optimization on handling of library state.Gravatar Maxime Dénès2017-03-22
| |\ \
| | | * [pp] [ide] Minor cleanups in pp code.Gravatar Emilio Jesus Gallego Arias2017-03-21
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | - We avoid unnecessary use of Pp -> string conversion functions. and the creation of intermediate buffers on logging. - We rename local functions that share the name with the Coq stdlib, this is usually dangerous as if the normal function is removed, code may pick up the one in the stdlib, with different semantics.
| | | * [error] Move back fatal_error to toplevelGravatar Emilio Jesus Gallego Arias2017-03-21
| | |/ | |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | This reverts 4444768d3f4f9c4fcdd440f7ab902886bd8e2b09 (the mllib dependencies that should be surely tweaked more). The logic for `fatal_error` has no place in `CErrors`, this is coqtop-specific code. What is more, a libobject caller should handle the exception correctly, I fail to see why the fix was needed on the first place.
| * | [safe_string] library/nameopsGravatar Emilio Jesus Gallego Arias2017-03-14
| | | | | | | | | | | | | | | | | | We add a more convenient API to create identifiers from mutable strings. We cannot solve the `String.copy` deprecation problem until we enable `-safe-string`.
| | * [library] Refactor state handling.Gravatar Emilio Jesus Gallego Arias2017-03-14
| | | | | | | | | | | | | | | This part of state is critical. We refactor it and make it into a record to ease handling.
| | * [library] Don't recompute path_prefix on unfreeze.Gravatar Emilio Jesus Gallego Arias2017-03-14
| |/ | | | | | | We instead save the current value.
* | Merge branch 'master'.Gravatar Pierre-Marie Pédrot2017-02-14
|\|
* | Namegen primitives now apply on evar constrs.Gravatar Pierre-Marie Pédrot2017-02-14
| | | | | | | | | | | | Incidentally, this fixes a printing bug in output/inference.v where the displayed name of an evar was the wrong one because its type was not evar-expanded enough.
| * 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
| | |
generated by cgit v1.2.3 (git 2.39.1) at 2024-12-03 11:10:27 +0000