aboutsummaryrefslogtreecommitdiffhomepage
path: root/library
Commit message (Collapse)AuthorAge
* Bump year in headers.Gravatar Maxime Dénès2017-06-01
|
* 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.
* 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.
* | 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).
* | 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.
* | 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
|/
* 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.
* Remove dead code in library/lib.ml.Gravatar Maxime Dénès2016-09-20
|
* 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
|
* Emit a warning on Require inside a module.Gravatar Maxime Dénès2016-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.
* 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
|
* COMMENT: moving misplaced comment where it belongsGravatar Matej Kosik2016-07-29
|
* errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib ↵Gravatar Pierre Letouzey2016-07-03
| | | | | | module) For the moment, there is an Error module in compilers-lib/ocamlbytecomp.cm(x)a
* Separate flags for fix/cofix/match reduction and clean reduction function names.Gravatar Maxime Dénès2016-07-01
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This is a reimplementation of Hugo's PR#117. We are trying to address the problem that the name of some reduction functions was not saying what they were doing (e.g. whd_betadeltaiota was doing let-in reduction). Like PR#117, we are careful that no function changed semantics without changing the names. Porting existing ML code should be a matter of renamings a few function calls. Also, we introduce more precise reduction flags fMATCH, fFIX, fCOFIX collectively denominated iota. We renamed the following functions: Closure.betadeltaiota -> Closure.all Closure.betadeltaiotanolet -> Closure.allnolet Reductionops.beta -> Closure.beta Reductionops.zeta -> Closure.zeta Reductionops.betaiota -> Closure.betaiota Reductionops.betaiotazeta -> Closure.betaiotazeta Reductionops.delta -> Closure.delta Reductionops.betalet -> Closure.betazeta Reductionops.betadelta -> Closure.betadeltazeta Reductionops.betadeltaiota -> Closure.all Reductionops.betadeltaiotanolet -> Closure.allnolet Closure.no_red -> Closure.nored Reductionops.nored -> Closure.nored Reductionops.nf_betadeltaiota -> Reductionops.nf_all Reductionops.whd_betadelta -> Reductionops.whd_betadeltazeta Reductionops.whd_betadeltaiota -> Reductionops.whd_all Reductionops.whd_betadeltaiota_nolet -> Reductionops.whd_allnolet Reductionops.whd_betadelta_stack -> Reductionops.whd_betadeltazeta_stack Reductionops.whd_betadeltaiota_stack -> Reductionops.whd_all_stack Reductionops.whd_betadeltaiota_nolet_stack -> Reductionops.whd_allnolet_stack Reductionops.whd_betadelta_state -> Reductionops.whd_betadeltazeta_state Reductionops.whd_betadeltaiota_state -> Reductionops.whd_all_state Reductionops.whd_betadeltaiota_nolet_state -> Reductionops.whd_allnolet_state Reductionops.whd_eta -> Reductionops.shrink_eta Tacmach.pf_whd_betadeltaiota -> Tacmach.pf_whd_all Tacmach.New.pf_whd_betadeltaiota -> Tacmach.New.pf_whd_all And removed the following ones: Reductionops.whd_betaetalet Reductionops.whd_betaetalet_stack Reductionops.whd_betaetalet_state Reductionops.whd_betadeltaeta_stack Reductionops.whd_betadeltaeta_state Reductionops.whd_betadeltaeta Reductionops.whd_betadeltaiotaeta_stack Reductionops.whd_betadeltaiotaeta_state Reductionops.whd_betadeltaiotaeta They were unused and having some reduction functions perform eta is confusing as whd_all and nf_all don't do it.
* Exporting section_segment_of_reference.Gravatar Hugo Herbelin2016-06-29
|
* universes.ml: Minor code cleanupGravatar Matthieu Sozeau2016-06-29
|
* A new infrastructure for warnings.Gravatar Maxime Dénès2016-06-29
| | | | | | | | | | | | | | | | | | | | | | | | | | On the user side, coqtop and coqc take a list of warning names or categories after -w. No prefix means activate the warning, a "-" prefix means deactivate it, and "+" means turn the warning into an error. Special categories include "all", and "default" which contains the warnings enabled by default. We also provide a vernacular Set Warnings which takes the same flags as argument. Note that coqc now prints warnings. The name and category of a warning are printed with the warning itself. On the developer side, Feedback.msg_warning is still accessible, but the recommended way to print a warning is in two steps: 1) create it by: let warn_my_warning = CWarnings.create ~name:"my-warning" ~category:"my-category" (fun args -> Pp.strbrk ...) 2) print it by: warn_my_warning args
* Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-06-27
|\
* | Reuse the typing_flags datatype for inductives.Gravatar Pierre-Marie Pédrot2016-06-18
| |
* | Moving the typing_flags to the environment.Gravatar Pierre-Marie Pédrot2016-06-18
| |
* | Adding a local type-in-type flag in kernel declarations.Gravatar Pierre-Marie Pédrot2016-06-18
| |
* | Factorizing the uses of Declareops.safe_flags.Gravatar Pierre-Marie Pédrot2016-06-16
| | | | | | | | | | This allows a smooth addition of various unsafe flags without wreaking havoc in the ML codebase.
* | Merge PR #79: Let the kernel assume that a (co-)inductive type is positive.Gravatar Pierre-Marie Pédrot2016-06-16
|\ \
| * | Assume totality: dedicated type rather than boolGravatar Arnaud Spiwack2016-06-14
| | | | | | | | | | | | | | | | | | | | | The rational is that 1. further typing flags may be available in the future 2. it makes it easier to trace and document the argument
* | | Merge remote-tracking branch 'origin/pr/166' into trunkGravatar Enrico Tassi2016-06-14
|\ \ \ | | | | | | | | | | | | Add -o option to coqc
* \ \ \ Merge branch "LtacProf for trunk" (PR #165).Gravatar Pierre-Marie Pédrot2016-06-14
|\ \ \ \
* | | | | Univs: more robust Universe/Constraint decls #4816Gravatar Matthieu Sozeau2016-06-13
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This fixes the declarations of constraints, universes and assumptions: - global constraints can refer to global universes only, - polymorphic universes, constraints and assumptions can only be declared inside sections, when all the section's variables/universes are polymorphic as well. - monomorphic assumptions may only be declared in section contexts which are not parameterized by polymorphic universes/assumptions. Add fix for part 1 of bug #4816
| | | | * Univs: fix for part #2 of bug #4816.Gravatar Matthieu Sozeau2016-06-13
| | | | | | | | | | | | | | | | | | | | | | | | | Check that the polymorphic status of everything that is parameterized in nested sections is coherent.
* | | | | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-06-09
|\ \ \ \ \ | | |_|_|/ | |/| | |
| | * | | LtacProf for Coq trunkGravatar Jason Gross2016-06-05
| |/ / / |/| | | | | | | | | | | | | | | | | | | This add LtacProfiling. Much of the code was written by Tobias Tebbi (@tebbi), and Paul A. Steckler was invaluable in porting the code to Coq v8.5 and Coq trunk.
| * | | Fix incorrect checking of library checksums.Gravatar Maxime Dénès2016-06-05
| | | | | | | | | | | | | | | | | | | | | | | | Since d09def34, only the summary of libraries was included in the checksum, not the actual content of the library. This quick fix performs the checking of the checksum immediately, even if the loading is delayed.
* | | | Feedback cleanupGravatar Emilio Jesus Gallego Arias2016-05-31
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This patch splits pretty printing representation from IO operations. - `Pp` is kept in charge of the abstract pretty printing representation. - The `Feedback` module provides interface for doing printing IO. The patch continues work initiated for 8.5 and has the following effects: - The following functions in `Pp`: `pp`, `ppnl`, `pperr`, `pperrnl`, `pperr_flush`, `pp_flush`, `flush_all`, `msg`, `msgnl`, `msgerr`, `msgerrnl`, `message` are removed. `Feedback.msg_*` functions must be used instead. - Feedback provides different backends to handle output, currently, `stdout`, `emacs` and CoqIDE backends are provided. - Clients cannot specify flush policy anymore, thus `pp_flush` et al are gone. - `Feedback.feedback` takes an `edit_or_state_id` instead of the old mix. Lightly tested: Test-suite passes, Proof General and CoqIDE seem to work.
| | * | coqc: support -o option to specify output file nameGravatar Enrico Tassi2016-05-19
| |/ / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | The -o option lets one put .vo or .vio files in a directory of choice, i.e. decouple the location of the sources and the compiled files. This ease the integration of Coq in already existing IDEs that handle the build process automatically (eg Eclipse) and also enables one to compile/run at the same time 2 versions of Coq on the same sources. Example: b.v depending on a.v coq8.6/bin/coqc -R out8.6 Test src/a.v -o out8.6/a.vo coq8.6/bin/coqc -R out8.6 Test src/b.v -o out8.6/b.vo coq8.7/bin/coqc -R out8.7 Test src/a.v -o out8.7/a.vo coq8.7/bin/coqc -R out8.7 Test src/b.v -o out8.7/b.vo
* | | Dyn: simplify API introducing an Easy submoduleGravatar Enrico Tassi2016-05-13
| | | | | | | | | | | | Now the casual Dyn user does not need to be a GADT guru
* | | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-05-09
|\| |
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-30 18:27:04 +0000