aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/output
Commit message (Collapse)AuthorAge
* 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
| | * | | add test for Show with -emacs, bug 5535Gravatar Paul Steckler2017-05-19
| | | | |
* | | | | A fix for #5390 (a useful error on used introduction names was masked).Gravatar Hugo Herbelin2017-05-17
|/ / / / | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | With the "apply in" introduction pattern, and the backtrack possibly done in "apply" over the components of conjunctions (descend_in_conjunctions), the reasons for failing might have different sources. We give priority to the detection of used names over other (unification) errors so that an error there is not masked in the backtracking made by descend_in_conjunctions. Of course, the question of what best unification error to give in the presence of backtracking is still open.
| | * / Fixing bug #5526,allow nonlinear variables in Notation patternsGravatar Paul Steckler2017-05-17
| |/ /
* | | Merge PR#457: Adding an even more compact goal hyps mode.Gravatar Maxime Dénès2017-05-17
|\ \ \
* \ \ \ Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2017-05-17
|\ \ \ \ | | |/ / | |/| |
| | * | Simplified compaction criterion + tests.Gravatar Pierre Courtieu2017-05-16
| |/ / |/| |
| * | remove unneeded -emacs flag to coq-prog-argsGravatar Paul Steckler2017-05-01
| | |
* | | Remove VernacErrorGravatar Gaetan Gilbert2017-04-21
| | |
* | | Merge PR#422: Supporting all kinds of binders, including 'pat, in syntax of ↵Gravatar Maxime Dénès2017-04-12
|\ \ \ | | | | | | | | | | | | record fields.
| | | * Better support for printing constructors with let-ins.Gravatar Hugo Herbelin2017-04-07
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This allows e.g. to use the record notations even when there are defined fields. A priori fixed also missing parameters when interpreting primitive tokens.
| | | * Fixing #4499 (not using unnamed record field in {| |} notation).Gravatar Hugo Herbelin2017-04-07
| | |/
* | | Merge branch 'master' into econstrGravatar Pierre-Marie Pédrot2017-04-07
|\ \ \
| * | | [toplevel] Remove exception error printer in favor of feedback printer.Gravatar Emilio Jesus Gallego Arias2017-04-05
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | We solve https://coq.inria.fr/bugs/show_bug.cgi?id=4789 by printing all the errors from the feedback handler, even in the case of coqtop. All error display is handled by a single, uniform path. There may be some minor discrepancies with 8.6 as we are uniform now whereas 8.6 tended to print errors in several ways, but our behavior is a subset of the 8.6 behavior. We had to make a choice for `-emacs` error output, which used to vary too. We have chosen to display error messages as: ``` (location info) option \n (program caret) option \n MARKER[254]Error: msgMARKER[255] ``` This commit also fixes: - https://coq.inria.fr/bugs/show_bug.cgi?id=5418 - https://coq.inria.fr/bugs/show_bug.cgi?id=5429
* | | | Merge branch 'trunk' into pr379Gravatar Maxime Dénès2017-04-04
|\| | |
| * | | Merge branch 'v8.6' into trunkGravatar Maxime Dénès2017-04-03
| |\ \ \ | | | |/ | | |/|
| | * | Instances should obey universe binders even when defined by tactics.Gravatar Gaetan Gilbert2017-04-03
| | | |
| * | | Merge PR#417: No cast surgery in let inGravatar Maxime Dénès2017-04-03
| |\ \ \
| * \ \ \ Merge branch 'v8.6' into trunkGravatar Maxime Dénès2017-03-30
| |\ \ \ \ | | | |/ / | | |/| |
| | * | | Run non-tactic comands without resilient_commandGravatar Tej Chajed2017-03-29
| | | | |
* | | | | Merge branch 'trunk' into pr379Gravatar Maxime Dénès2017-03-24
|\| | | |
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-04 14:23:09 +0000