aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/output
Commit message (Expand)AuthorAge
* 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
* | | | | | 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
| | | | | * Unification constraint handling (#4763, #5149)Gravatar Matthieu Sozeau2016-10-22
| | |_|_|/ | |/| | |
| * | | | Revert 214b9ab7969fae71dcf553c399cb1674e463d0e3Gravatar Matthieu Sozeau2016-10-21
| * | | | [search] Don't build intermediate lists in search.Gravatar Emilio Jesus Gallego Arias2016-10-20
| * | | | 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
| | | | * [pp] Try to properly tag error messages in cError.Gravatar Emilio Jesus Gallego Arias2016-10-18
| | |_|/ | |/| |