aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/output
Commit message (Collapse)AuthorAge
* Pre-isolating a notation test to avoid interferences.Gravatar Hugo Herbelin2017-11-27
|
* Fixes #5787 (printing of "constr:" lost in the move of constr to Generic).Gravatar Hugo Herbelin2017-11-20
| | | | Was broken since 8.6.
* Binding ltac printing functions to the system of generic printing.Gravatar Hugo Herbelin2017-11-02
| | | | | | | | | | This concerns pr_value and message_of_value. This has a few consequences. For instance, no more ad hoc message "a term" or "a tactic", when not enough information is available for printing, one gets a generic message "a value of type foobar". But we also have more printers, satisfying e.g. request #5786.
* Moving bug numbers to BZ# format in the test-suite.Gravatar Théo Zimmermann2017-10-19
| | | | | Compared to the original proposition (59a594b in #960), this commit only changes files containing bug numbers that are also PR numbers.
* Use a nice printer for constant names in Suggest Proof Using.Gravatar Gaëtan Gilbert2017-10-10
|
* Take Suggest Proof Using outside the kernel.Gravatar Gaëtan Gilbert2017-10-10
| | | | | | | | | | | | | | | | | | | Also add an output test for Suggest Proof Using. This changes the .aux output: instead of getting a key >context_used "$hyps;$suggest" where $hyps is a list of the used hypotheses and $suggest is the ;-separated suggestions (or the empty string if Suggest Proof Using is unset), there is a key >context_used "$hyps" and if Suggest Proof Using is set also a key >suggest_proof_using "$suggest" For instance instead of 112 116 context_used "B A;A B;All" we get 112 116 context_used "B A" 112 116 suggest_proof_using "A B;All"
* Merge PR #1062: BZ#5739, Allow level for leftmost nonterminal for ↵Gravatar Maxime Dénès2017-10-09
|\ | | | | | | printing-ony Notations
* \ Merge PR #1078: Report missing arguments in error messageGravatar Maxime Dénès2017-10-04
|\ \
* \ \ Merge PR #1058: Fixing BZ#5741 (anomaly in info_trivial).Gravatar Maxime Dénès2017-10-04
|\ \ \
| | | * BZ#5739, Allow level for leftmost nonterminal for printing-ony NotationsGravatar Paul Steckler2017-09-25
| | | |
| | * | Report missing arguments in error messageGravatar Tej Chajed2017-09-21
| | |/ | | | | | | | | | | | | | | | | | | Augment the "Illegal tactic application" error message with the number of extra arguments passed. Fixes BZ#5753.
| * / Fixing bug #5741 (anomaly in info_trivial).Gravatar Hugo Herbelin2017-09-19
| |/ | | | | | | The bug was introduced in 1559f73.
* / Don't lose names in UState.universe_context.Gravatar Gaëtan Gilbert2017-09-19
|/ | | | | We dont care about the order of the binder map ([map] in the code) so no need to do tricky things with it.
* Merge PR #986: Ensuring all .v files end with a newline to make "sed -i" ↵Gravatar Maxime Dénès2017-09-15
|\ | | | | | | work better on them
* | Fixing bug #5693 (treating empty notation format as any format).Gravatar Hugo Herbelin2017-09-12
| | | | | | | | | | A trick in counting spaces in a format was making the empty notation not behaving correctly.
* | Fixing a bug of recursive notations introduced in dfdaf4de.Gravatar Hugo Herbelin2017-09-12
| | | | | | | | | | | | | | | | When a proper notation variable occurred only in a recursive pattern of the notation, the notation was wrongly considered non printable due (the side effect that function compare_glob_constr and that mk_glob_constr_eq does not do anymore was indeed done by aux' but thrown away). This fixes it.
* | Adding a test for #5569 (warning about skipping spaces).Gravatar Hugo Herbelin2017-08-29
| | | | | | | | The two previous commits make the warning irrelevant and useless.
* | A little reorganization of notations + a fix to #5608.Gravatar Hugo Herbelin2017-08-29
| | | | | | | | | | | | | | | | | | | | | | | | | | | | - Formerly, notations such as "{ A } + { B }" were typically split into "{ _ }" and "_ + _". We keep the split only for parsing, which is where it is really needed, but not anymore for interpretation, nor printing. - As a consequence, one notation string can give rise to several grammar entries, but still only one printing entry. - As another consequence, "{ A } + { B }" and "A + { B }" must be reserved to be used, which is after all the natural expectation, even if the sublevels are constrained. - We also now keep the information "is ident", "is binder" in the "key" characterizing the level of a notation.
| * Ensuring all .v files end with a newline to make "sed -i" work better on them.Gravatar Hugo Herbelin2017-08-21
|/
* Print names of all open blocksGravatar Tej Chajed2017-08-06
| | | | Fixes bug 5597.
* Merge PR #834: Adding support for recursive notations of the form "x , .. , ↵Gravatar Maxime Dénès2017-08-01
|\ | | | | | | y , z".
* | Fix TypeclassDebug.out after conflicting PR mergesGravatar Matthieu Sozeau2017-07-26
| |
| * Adding support for recursive notations of the form "x , .. , y , z".Gravatar Hugo Herbelin2017-07-26
|/ | | | | | | | | Since camlp5 parses from left, the last ", z" was parsed as part of an arbitrary long list of "x1 , .. , xn" and a syntax error was raised since an extra ", z" was still expected. We support this by translating "x , .. , y , z" into "x , y , .. , z" and reassembling the arguments appropriately after parsing.
* Merge PR #869: Enforce alternating separators in typeclass debug outputGravatar Maxime Dénès2017-07-20
|\
| * format pairs of items for pr_depth to get alternating separatorsGravatar Paul Steckler2017-07-12
| | | | | | | | | | eval thunks once in prlist_sep_lastsep, make code clearer add typeclass debug output test
* | Deprecate options that were introduced for compatibility with 8.5.Gravatar Théo Zimmermann2017-07-11
|/
* Merge PR #863: Fixing environment in warning "Projection value has no head ↵Gravatar Maxime Dénès2017-07-07
|\ | | | | | | constant".
| * Fixing environment in warning "Projection value has no head constant".Gravatar Hugo Herbelin2017-07-07
| | | | | | | | | | Delaying also some computation needed for printing to the time of really printing it.
* | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2017-07-04
|\ \ | |/ |/|
| * Add tests for handling of warningsGravatar Tej Chajed2017-06-23
| |
* | Merge PR#513: A fix to #5414 (ident bound by ltac names now known for "match").Gravatar Maxime Dénès2017-06-14
|\ \
* | | Prelude : no more autoload of plugins extraction and recdefGravatar Pierre Letouzey2017-06-14
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | The user now has to manually load them, respectively via: Require Extraction Require Import FunInd The "Import" in the case of FunInd is to ensure that the tactics functional induction and functional inversion are indeed in scope. Note that the Recdef.v file is still there as well (it contains complements used when doing Function with measures), and it also triggers a load of FunInd.v. This change is correctly documented in the refman, and the test-suite has been adapted.
* | | BigNums: remove files about BigN,BigZ,BigQ (now in an separate git repo)Gravatar Pierre Letouzey2017-06-13
| | | | | | | | | | | | | | | | | | See now https://github.com/coq/bignums Int31 is still in the stdlib. Some proofs there has be adapted to avoid the need for BigNumPrelude.
| | * Fix Bug #5568, no dup notation warnings on repeated module importsGravatar Paul Steckler2017-06-09
| | |
| * | A fix to #5414 (ident bound by ltac names now known for "match").Gravatar Hugo Herbelin2017-06-09
|/ / | | | | | | | | | | | | | | | | Also taking into account a name in the return clause and in the indices. Note the double meaning ``bound as a term to match'' and ``binding in the "as" clause'' when the term to match is a variable for all of "match", "if" and "let".
* | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2017-06-08
|\|
* | Merge PR#647: [emacs] [toplevel] Make emacs flag local to the toplevel.Gravatar Maxime Dénès2017-06-02
|\ \
| * | [emacs] [toplevel] Make emacs flag local to the toplevel.Gravatar Emilio Jesus Gallego Arias2017-06-01
| | | | | | | | | | | | | | | We remove the emacs-specific printing code from the core of Coq, now `-emacs` is a printing flag controlled by the toplevel.
* | | Merge PR#694: Fixing #5523 (missing support for complex constructions in ↵Gravatar Maxime Dénès2017-06-01
|\ \ \ | |/ / |/| | | | | recursive notations) (bis)
| * | Fixing a too lax constraint for finding recursive binder part of a notation.Gravatar Hugo Herbelin2017-05-31
| | | | | | | | | | | | | | | | | | This was preventing to work examples such as: Notation "[ x ; .. ; y ; z ]" := ((x,((fun u => u), .. (y,(fun u =>u,z)) ..))).
* | | Support for using type information to infer more precise evar sources.Gravatar Hugo Herbelin2017-05-30
|/ / | | | | | | | | | | | | | | This allows a better control on the name to give to an evar and, in particular, to address the issue about naming produced by "epose proof" in one of the comment of Zimmi48 at PR #248 (see file names.v). Incidentally updating output of Show output test (evar numbers shifted).
| * Merge PR#546: Fix for bug #4499 and other minor related bugsGravatar Maxime Dénès2017-05-29
| |\
| * \ Merge PR#679: Bug 5546, qualify datatype constructors when needed in Show MatchGravatar Maxime Dénès2017-05-28
| |\ \
| * \ \ Merge PR#634: Fix bug #5526, don't check for nonlinearity in notation if ↵Gravatar Maxime Dénès2017-05-26
| |\ \ \ | | | | | | | | | | | | | | | printing only
* | | | | add Show test with -emacs flagGravatar Paul Steckler2017-05-25
| | | | |
| | | * | Bug 5546, qualify datatype constructors when neededGravatar Paul Steckler2017-05-25
| | |/ / | |/| |
* | | | Merge PR#661: Added a test for #4765 (an example of printing abbreviation ↵Gravatar Maxime Dénès2017-05-23
|\ \ \ \ | | | | | | | | | | | | | | | with binders)
* \ \ \ \ Merge PR#657: [test-suite] Add tests for goal printing.Gravatar Maxime Dénès2017-05-23
|\ \ \ \ \
| | * | | | Added a test for #4765 (an example of printing abbreviation with binders).Gravatar Hugo Herbelin2017-05-20
| |/ / / / |/| | | |
| * | | | [test-suite] Add tests for goal printing.Gravatar Emilio Jesus Gallego Arias2017-05-20
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | - https://coq.inria.fr/bugs/show_bug.cgi?id=5529 - https://coq.inria.fr/bugs/show_bug.cgi?id=5537 See also PR #640
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-06 21:58:54 +0000