aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/output
Commit message (Expand)AuthorAge
* Merge PR #834: Adding support for recursive notations of the form "x , .. , y...Gravatar Maxime Dénès2017-08-01
|\
* | 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
|/
* 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
* | 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 co...Gravatar Maxime Dénès2017-07-07
|\
| * Fixing environment in warning "Projection value has no head constant".Gravatar Hugo Herbelin2017-07-07
* | 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
* | | BigNums: remove files about BigN,BigZ,BigQ (now in an separate git repo)Gravatar Pierre Letouzey2017-06-13
| | * 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
|/ /
* | 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
* | | 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
|/ /
| * 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 prin...Gravatar Maxime Dénès2017-05-26
| |\ \ \
* | | | | 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 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
| | * | | 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
|/ / / /
| | * / 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 r...Gravatar Maxime Dénès2017-04-12
|\ \ \
| | | * Better support for printing constructors with let-ins.Gravatar Hugo Herbelin2017-04-07
| | | * 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
* | | | 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
|\| | | |