aboutsummaryrefslogtreecommitdiffhomepage
path: root/toplevel
Commit message (Collapse)AuthorAge
* Merge remote-tracking branch 'github/pr/366' into v8.6Gravatar Maxime Dénès2016-12-04
|\ | | | | | | Was PR#366: Univs: fix bug 5208
* | Comment on universe handling in ParametersGravatar Matthieu Sozeau2016-12-02
| |
* | Univs: fix bug #5188Gravatar Matthieu Sozeau2016-12-02
| | | | | | | | | | Parameter was implemented the wrong way trying to separate the universes of the telescope.
| * Fix UGraph.check_eq!Gravatar Matthieu Sozeau2016-11-30
|/ | | | | | | | | | | | | | | | | Universes are kept in normal form w.r.t. equality but not the <= relation, so the previous check worked almost always but was actually too strict! In cases like (max(Set,u) = u) when u is declared >= Set it was failing to find an equality. Applying the KISS principle: u = v <-> u <= v /\ v <= u. Fix invariant breakage that triggered the discovery of the check_eq bug as well. No algebraic universes should appear in a term position (on the left of a colon in a typing judgment), this was not the case when an algebraic universe instantiated an evar that appeared in the term. We force their universe variable status to change in refresh_universes to avoid this. Fix ind sort inference: Use syntactic universe equality for inductive sort inference instead of check_leq (which now correctly takes constraints into account) and simplify code
* 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.
* Stop parsing -compat-notations options, which are no longer supported (bug ↵Gravatar Guillaume Melquiond2016-11-21
| | | | #3339).
* Revert "Merge remote-tracking branch 'github/pr/360' into v8.6"Gravatar Maxime Dénès2016-11-18
| | | | | | | | | This reverts commit b00e039b957b8428c21faec5c76f3a3484cde2cf, reversing changes made to ca9e00ff9b2a8ee17430398a5e0bef2345c39341. It turns out that calling from fake_ide the STM commands that were removed by this PR requires an extension of the XML protocol. So postponing the integration.
* [stm] Remove STM-related vernacularsGravatar Emilio Jesus Gallego Arias2016-11-17
| | | | | | | | | I think these commands never make a lot of sense on scripts other than debugging and we have better methods now. The last remaining command, used for the tty emulation has been renamed to VtBack, but it should go away at some point too once the legacy interfaces are removed.
* Fix bug in warnings: -w foo was silent when foo did not exist.Gravatar Maxime Dénès2016-11-14
|
* Do not mention "none" in warnings doc, as it is there for compatibility.Gravatar Maxime Dénès2016-11-14
|
* Merge remote-tracking branch 'github/pr/339' into v8.6Gravatar Maxime Dénès2016-11-07
|\ | | | | | | Was PR#339: Documenting type class options, typeclasses eauto
| * Fixes to compile with ocaml 4.01Gravatar Matthieu Sozeau2016-11-07
| |
* | Merge commit 'e6edb33' into v8.6Gravatar Maxime Dénès2016-11-07
|\ \ | | | | | | | | | Was PR#331: Solve_constraints and Set Use Unification Heuristics
* | | Improve formatting of a message in [Arguments].Gravatar Maxime Dénès2016-11-07
| | |
* | | Fix #5181: [Arguments] no longer correctly checks the length of arguments listsGravatar Maxime Dénès2016-11-07
| | |
* | | Fix #5182: "Arguments names must be distinct." is bogus and underinformativeGravatar Maxime Dénès2016-11-07
| | |
* | | Not using style tags when translating/beautifying a file.Gravatar Hugo Herbelin2016-11-05
| | |
* | | Quick fix of tactic parsing while Load-ing in coqide.Gravatar Hugo Herbelin2016-11-04
| | | | | | | | | | | | Note that this is still broken when loading files containing C-zar scripts.
* | | Add documentation for [Set Warnings] and the -w option.Gravatar Cyprien Mangin2016-11-04
| | |
| | * Lets Hints/Instances take an optional patternGravatar Matthieu Sozeau2016-11-03
| | | | | | | | | | | | | | | | | | | | | | | | | | | In addition to a priority, cleanup the interfaces for passing this information as well. The pattern, if given, takes priority over the inferred one. We only allow Existing Instances gr ... gr | pri. for now, without pattern, as before. Make the API compatible to 8.5 as well.
* | | 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).
* | | Removing dead code.Gravatar Hugo Herbelin2016-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
* \ \ Merge remote-tracking branch 'github/pr/337' into v8.6Gravatar Maxime Dénès2016-10-28
|\ \ \ | | | | | | | | | | | | Was PR#337: Fix arguments
| * | | 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.5' into v8.6Gravatar Pierre-Marie Pédrot2016-10-26
|\ \ \ \
| | | | * Renamings to avoid confusion deprecating old namesGravatar Matthieu Sozeau2016-10-22
| |_|_|/ |/| | | | | | | | | | | | | | | reconsider_conv_pbs -> reconsider_unif_constraints consider_remaining_unif_problems -> solve_unif_constraints_with_heuristics
| * | | Fix a bug in error printing of unif constraintsGravatar Matthieu Sozeau2016-10-22
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Conversion problems are in a de Bruijn environment that may include references to unbound rels (because of the way evars are created), we patch the env to named all de Bruijn variables so that error printing does not raise an anomaly. Also fix a minor printing bug in unsatisfiable constraints error reporting. HoTT_coq_117.v tests all of this.
* | | | [search] Don't build intermediate lists in search.Gravatar Emilio Jesus Gallego Arias2016-10-20
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This patch converts the `search_*` functions to use an iter-style API. Consequently, the Search Vernac will produce a message for each search result, greatly improving roundtrip time as IDEs can effectively display the results in a streaming way. It also allows different printers to be used. I didn't observe a performance difference (as things seem to be dominated by printing and `Declaremods`). As a minor tweak, we make search with "Output Name Only" more efficient. Motivation: ----------- Currently, the main search API `Search.generic_search` is an effectful, iteration-based function: ```ocaml val generic_search : int option -> display_function -> unit ``` This type is imposed by `Declaremods`, which exposes an effectful, iteration-based API to traverse Coq library objects. The `Search.search_*` functions try to offer a more functional API by returning a list of pretty printing commands. They need to build an internal intermediate list for that purpose. However, this is a waste of time, as the destination of these lists is to be flushed out by the printer right away.
| | | * [pp] Add tagging function to all low-level printing calls.Gravatar Emilio Jesus Gallego Arias2016-10-18
| |_|/ |/| | | | | | | | | | | | | | | | | | | | The current tag system in `Pp` is generic, which implies we must choose a tagging function when calling a printer. For console printing there is a single choice, thus this commits adds it a few missing cases.
* | | [toplevel] Remove undocumented "just_parsing" flag.Gravatar Emilio Jesus Gallego Arias2016-10-17
| | | | | | | | | | | | | | | It was not very useful as just parsing won't get you very far due to lack of notation loading.
* | | [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/`.
* | | Vernac.ml: inlining read_vernac_file within load_vernac.Gravatar Hugo Herbelin2016-10-17
| | | | | | | | | | | | | | | | | | Also renaming vernac_com into interp_vernac and eval_expr into process_vernac to clarify that it does side-effects (on the contrary of Stm.interp/Vernacentries.interp).
* | | Grouping checks about commands together.Gravatar Hugo Herbelin2016-10-17
| | |
* | | Vernac.ml: parenthesizing a side-effect.Gravatar Hugo Herbelin2016-10-17
| | | | | | | | | | | | | | | Moving set_formatter_out_channel where it naturally closes the corresponding opening set_formatter_output_functions.
* | | Factorizing two instances of load_vernac.Gravatar Hugo Herbelin2016-10-17
| | |
* | | Passing chan_beautify functionally rather than by side-effect.Gravatar Hugo Herbelin2016-10-17
| | |
* | | Applying Emilio's suggestion to simplify type of eval_expr.Gravatar Hugo Herbelin2016-10-17
| | | | | | | | | | | | | | | | | | | | | This is not fully satisfactory though since we would not like to have "eval_expr" depending on a parsing/lexing/comments state... but it does because of eval_expr possibly printing the vernac expression given to it.
* | | More on making the lexer more functional (continuing b8ae2de5 andGravatar Hugo Herbelin2016-10-17
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 8a8caba3). - Adding cLexer.current_file to the lexer state, i.e. making it a component of the type "coq_parsable" of lexer state (it was forgotten in b8ae2de5 and 8a8caba3). - Inlining save_translator/restore_translator which have now lost most of their substance.
* | | Removing export of location_table outside of cLexer.Gravatar Hugo Herbelin2016-10-17
| | | | | | | | | | | | | | | | | | | | | It was not used any more by coqdoc since b8194b22 (Dec 2010). The table is now only part of the lexer function closure (and only in the camlp5 case).
* | | Fix bug #5141: Bogus message "Error: Cannot infer type of pattern-matching".Gravatar Pierre-Marie Pédrot2016-10-16
| |/ |/| | | | | | | | | | | We simply explicit that the type is actually referring to the return type, not to the type of the argument of the pattern-matching. Note that the heuristic could be enhanced so as to use the same code in both let-style and match-style pattern-matching, but I'm leaving this for another time.
* | Merge PR #224 into v8.6Gravatar Pierre-Marie Pédrot2016-10-12
|\ \
* | | Fixing #5133 (error reporting delayed).Gravatar Hugo Herbelin2016-10-10
| | | | | | | | | | | | | | | I wrongly moved call to the function interpreting commands within a different try-with block in 8a8caba36e.
| | * A tentative fix for #5102 (bullets parsing broken by calls to parse_entry).Gravatar Hugo Herbelin2016-10-09
| | | | | | | | | | | | | | | | | | | | | More precisely, commands that calls parse_entry put the lexer in an inconsistent state, breaking the lexing of bullet which relies on it. (Not to be pushed to v8.6 which has a better fix).
* | | 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.
* | | Attaching all extra imperative components of the lexer/parser state toGravatar Hugo Herbelin2016-10-09
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | the state of parsable streams, so that different lexing/parsing processes can be started independently without conflicting. Note however that these different lexing/parsing processes cannot be run concurrently as they still work on the same piece of global memory (i.e. calls to entry_parse should remain atomic). To go further, one would typically need to be able to functionally pass the lexing state to each call to the lexer. Note that currently the beautifier is also running in the context of a lexer/parser state (for the mapping of location to comments). In particular, this fixes #5102 (parsing/lexing of bullets depending on the lexing state which was global).
* | | Fixing beautification to file.Gravatar Hugo Herbelin2016-10-09
| | |
* | | Fix bug #5125: Bad error message when attempting to use where with Class.Gravatar Pierre-Marie Pédrot2016-10-07
| | |
* | | Remove the -no-compat-notations flag.Gravatar Maxime Dénès2016-10-06
| | | | | | | | | | | | | | | | | | This option was not doing anything... Today, one can turn the compatibility notations warning into an error, if ever that was the intended semantics.
* | | Remove the Set Verbose Compat option and turn the warning on by default.Gravatar Maxime Dénès2016-10-06
| | | | | | | | | | | | | | | These warnings can now be configured like any other, so we don't need a specific option anymore.
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-30 18:32:18 +0000