aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/output
Commit message (Expand)AuthorAge
* 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
* | Merge PR#694: Fixing #5523 (missing support for complex constructions in recu...Gravatar Maxime Dénès2017-06-01
|\ \ | |/ |/|
| * Fixing a too lax constraint for finding recursive binder part of a notation.Gravatar Hugo Herbelin2017-05-31
* | Support for using type information to infer more precise evar sources.Gravatar Hugo Herbelin2017-05-30
|/
* add Show test with -emacs flagGravatar Paul Steckler2017-05-25
* Merge PR#661: Added a test for #4765 (an example of printing abbreviation wit...Gravatar Maxime Dénès2017-05-23
|\
* \ 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
* | A fix for #5390 (a useful error on used introduction names was masked).Gravatar Hugo Herbelin2017-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 r...Gravatar Maxime Dénès2017-04-12
|\ \
* \ \ 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
* | | | 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
|\| | | |
| | | * | Applying same convention as in Definition for printing type in a let in.Gravatar Hugo Herbelin2017-03-24
| | |/ / | |/| |
| | | * A test checking for non-collision of name in irrefutable patterns.Gravatar Hugo Herbelin2017-03-23
| | |/ | |/|
| * | [pp] Make feedback the only logging mechanism.Gravatar Emilio Jesus Gallego Arias2017-03-21
| * | Report missing tactic arguments in error messageGravatar Tej Chajed2017-03-14
* | | Merge branch 'master'.Gravatar Pierre-Marie Pédrot2017-02-14
|\| |
* | | Namegen primitives now apply on evar constrs.Gravatar Pierre-Marie Pédrot2017-02-14
| * | Merge PR#253: Sort Search results by relevanceGravatar Maxime Dénès2017-02-14
| |\ \
| | * | Test-suite: output of SearchGravatar Arnaud Spiwack2017-02-14
| |/ / |/| |
| * | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2017-02-01
| |\|
| | * Merge branch 'v8.5' into v8.6Gravatar Pierre-Marie Pédrot2017-01-23
| | |\
| | | * Fixing a little bug in printing cofix with no arguments.Gravatar Hugo Herbelin2017-01-05
| * | | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-12-07
| |\| |
| | * | Fix test-suite after change in "context" printing.Gravatar Maxime Dénès2016-12-02
| * | | Tests for info/debug auto/eauto.Gravatar Hugo Herbelin2016-11-19
| * | | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-11-18
|/| | | | |/ /
| * | Updating a comment in test-suite.Gravatar Hugo Herbelin2016-11-10
| * | Merge commit 'e6edb33' into v8.6Gravatar Maxime Dénès2016-11-07
| |\ \
| * | | Fix #5182: "Arguments names must be distinct." is bogus and underinformativeGravatar Maxime Dénès2016-11-07
| | * | More explicit name for status of unification constraints.Gravatar Maxime Dénès2016-11-07
* | | | 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
| |\ \ \
| * \ \ \ Merge remote-tracking branch 'github/pr/337' into v8.6Gravatar Maxime Dénès2016-10-28
| |\ \ \ \
| | * | | | 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