aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/output
Commit message (Collapse)AuthorAge
* 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
| * \ 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
| | | |
| | * | 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
|\| | |
| * | | Adding a test for #4398 (interpretation scopes for "match goal").Gravatar Hugo Herbelin2016-10-24
| | | |
| * | | Merge branch 'v8.5' into v8.6Gravatar Hugo Herbelin2016-10-22
| |\ \ \
| | * | | Fixing printing of generic arguments of tag "var".Gravatar Hugo Herbelin2016-10-22
| | | | |
| * | | | Revert 214b9ab7969fae71dcf553c399cb1674e463d0e3Gravatar Matthieu Sozeau2016-10-21
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This makes [refine] typecheck the term only once (instead of twice), (Qed excluded of course). Fix test-suite file for output of constraints accordingly.
| * | | | [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.
| * | | | Test for variant of #5142 (good error message on pattern-matching failure).Gravatar Hugo Herbelin2016-10-19
| | | | |
| * | | | Attempt to improve error rendering in pattern-matching compilation (#5142).Gravatar Hugo Herbelin2016-10-19
| | | | | | | | | | | | | | | | | | | | | | | | | When trying different possible return predicates, returns the error given by the first try, assuming this is the most interesting one.
| | | | * [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
|\| | |
| | * | Removing output test for module qualification.Gravatar Pierre-Marie Pédrot2016-10-18
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | I do not know how to provide a proper test in 8.5, as the location on my machine appears in the error printed when loading the file. Adding a Fail on the End command does not help much either, because it simply does not print anything. Do not merge this commit in 8.6, we still want a test there.
| * | | Fixing a few other inconsistencies with notations.Gravatar Hugo Herbelin2016-10-17
| | | | | | | | | | | | | | | | | | | | `Notation ".a" := nat.' was accepted and used for printing but not recognized in parsing. Now it does. Other examples in test-suite.
* | | | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-10-17
|\| | |
| * | | Fix output test for module qualification.Gravatar Pierre-Marie Pédrot2016-10-17
| | | | | | | | | | | | | | | | The output was embedding local paths from my machine.
| * | | Merge PR #310 into v8.6Gravatar Pierre-Marie Pédrot2016-10-17
| |\| | | | |/ | |/|
| | * Test for bug #4874.Gravatar Pierre-Marie Pédrot2016-10-17
| | |
* | | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-10-02
|\| |
| * | Fix bug #4661: Cannot mask the absolute name.Gravatar Pierre-Marie Pédrot2016-10-01
| | | | | | | | | | | | | | | | | | The patch is quite dumb: it essentially consists in alpha-renaming bound module names when printing a functor, by checking that the name was not already present, and generating a fresh one otherwise.
| * | Merge branch 'v8.5' into v8.6Gravatar Maxime Dénès2016-09-30
| |\|
| | * Fix test-suite.Gravatar Maxime Dénès2016-09-30
| | | | | | | | | | | | Restore subst output test file modified by mistake.
| * | Ignore file names in warning emitted by test-suite/output/* (#5111)Gravatar Enrico Tassi2016-09-30
| | |
| * | Merge branch 'v8.5' into v8.6Gravatar Maxime Dénès2016-09-30
| |\|
| * | Arguments: cleanup + detect discrepancy rename/implicit (#3753)Gravatar Enrico Tassi2016-09-29
| | | | | | | | | | | | | | | It seems warnings are not taken into account in output/ tests.
| | * Fix a bug in subst releaved by an OCaml warning.Gravatar Maxime Dénès2016-09-29
| | |
| * | Argument : assert does fail if no arg is given (fix #4864)Gravatar Enrico Tassi2016-09-29
| | |
* | | Fixing test FunExt.v.Gravatar Hugo Herbelin2016-09-19
| | |
* | | extensionality: Handle dependently-used hypothesesGravatar Jason Gross2016-09-19
| | |
* | | Adding an "extensionality in H" tactic which applies functionalGravatar Hugo Herbelin2016-09-19
| | | | | | | | | | | | | | | | | | | | | | | | extensionality in H supposed to be a quantified equality until giving a bare equality. Thanks to Jason Gross and Jonathan Leivent for suggestions and examples.
* | | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-09-14
|\| |
| * | Merge branch 'v8.5' into v8.6Gravatar Pierre-Marie Pédrot2016-09-14
| |\|
| | * Fixing a recursive notation bug raised on coq-club on Sep 12, 2016.Gravatar Hugo Herbelin2016-09-12
| | |
| * | Merge remote-tracking branch 'github-coq/pr/249' into v8.6Gravatar Matthieu Sozeau2016-09-12
| |\ \
| | * | no-refold patchGravatar Paul Steckler2016-09-09
| | | | | | | | | | | | | | | | | | | | | | | | Add a boolean for refolding during reduction, and an option that is off by default in 8.6, to turn refolding on in all reduction functions, as in 8.5.
| * | | Fix output test-suite after commit 0d3c319.Gravatar Pierre-Marie Pédrot2016-09-09
| |/ /
* | | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-09-02
|\| |
| * | Fixing output test-suite after warning for inner Requires.Gravatar Pierre-Marie Pédrot2016-08-30
| | |
* | | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-07-20
|\| |
| | * Fix Errors.out missing a dot...Gravatar Matthieu Sozeau2016-07-19
| | |
| * | Some extra fixes in printing patterns in binders.Gravatar Hugo Herbelin2016-07-19
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | - typo in notation_ops.ml - factorization of patterns in ppconstr.ml - update of test-suite - printing of cast of a binding pattern if in mode "printing all" The question of whether or not to print the type of a binding pattern by default seems open to me.
| * | Taking into account binding patterns when agglutinating sequences of binders.Gravatar Hugo Herbelin2016-07-19
| | | | | | | | | | | | | | | Supporting accordingly printing of sequences of binders including binding patterns.
| * | Fixing missing parentheses in printing of patterns in binders.Gravatar Hugo Herbelin2016-07-19
| | | | | | | | | | | | (In agreement with Daniel.)
| * | Notations: fixing multiple binders used as terms in reverse order.Gravatar Hugo Herbelin2016-07-19
| | |
| * | Removing a source of clash with multiple recursive patterns in notations.Gravatar Hugo Herbelin2016-07-19
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | The same variable name was used to collect the binders and the successive steps of matching one binder, resulting in unexpected attempts for merging in the presence of multiple occurrence of the same recursive pattern. An amusing side-effect: when eta-expanding for a notation with recursive binders, it is the second variable of the "x .. y" which is used to invent a name rather than the first one.
| * | A new step on using alpha-conversion in printing notations.Gravatar Hugo Herbelin2016-07-18
| | | | | | | | | | | | | | | | | | | | | A couple of bugs have been found. Example #4932 is now printing correctly in the presence of multiple binders (when no let-in, no irrefutable patterns).
| * | Partial fix to #4592 (notation requiring alpha-conversion for printing).Gravatar Hugo Herbelin2016-07-17
| | |
generated by cgit v1.2.3 (git 2.39.1) at 2024-08-12 14:00:47 +0000