aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/output
Commit message (Expand)AuthorAge
* Merge branch 'v8.5' into v8.6Gravatar Pierre-Marie Pédrot2016-09-14
|\
| * Fixing a recursive notation bug raised on coq-club on Sep 12, 2016.Gravatar Hugo Herbelin2016-09-12
* | Merge remote-tracking branch 'github-coq/pr/249' into v8.6Gravatar Matthieu Sozeau2016-09-12
|\ \
| * | no-refold patchGravatar Paul Steckler2016-09-09
* | | Fix output test-suite after commit 0d3c319.Gravatar Pierre-Marie Pédrot2016-09-09
|/ /
* | Fixing output test-suite after warning for inner Requires.Gravatar Pierre-Marie Pédrot2016-08-30
| * Fix Errors.out missing a dot...Gravatar Matthieu Sozeau2016-07-19
* | Some extra fixes in printing patterns in binders.Gravatar Hugo Herbelin2016-07-19
* | Taking into account binding patterns when agglutinating sequences of binders.Gravatar Hugo Herbelin2016-07-19
* | Fixing missing parentheses in printing of patterns in binders.Gravatar Hugo Herbelin2016-07-19
* | Notations: fixing multiple binders used as terms in reverse order.Gravatar Hugo Herbelin2016-07-19
* | Removing a source of clash with multiple recursive patterns in notations.Gravatar Hugo Herbelin2016-07-19
* | A new step on using alpha-conversion in printing notations.Gravatar Hugo Herbelin2016-07-18
* | Partial fix to #4592 (notation requiring alpha-conversion for printing).Gravatar Hugo Herbelin2016-07-17
* | More examples of recursive notations, with emphasis in reference manual.Gravatar Hugo Herbelin2016-07-17
* | Fixing a bug in recognizing a recursive pattern of notationsGravatar Hugo Herbelin2016-07-17
* | Fixing interpretation of notations w/ opposite instances of a recursive pattern.Gravatar Hugo Herbelin2016-07-17
* | Fixing printing of notations with several instances of a recursive pattern.Gravatar Hugo Herbelin2016-07-17
* | Merge branch 'v8.5' into v8.6Gravatar Pierre-Marie Pédrot2016-07-13
|\|
| * Fixing printing of evar name in an error message of instantiate.Gravatar Hugo Herbelin2016-07-13
* | Fix issues in test-suite revealed by warnings.Gravatar Maxime Dénès2016-06-29
* | Adding a test-suite for the only printing flag.Gravatar Pierre-Marie Pédrot2016-06-28
* | Patterns in binders: printing testsGravatar Arnaud Spiwack2016-06-27
* | Adding ability to put any pattern in binders, prefixed by a quote.Gravatar Daniel de Rauglaudre2016-06-27
* | Fixing #4854 (regression introduced in 4d25b224 in relation with #4592).Gravatar Hugo Herbelin2016-06-24
* | Exporting a generic argument induction_arg. As a consequence,Gravatar Hugo Herbelin2016-06-18
* | proof mode: print unification constraintsGravatar Matthieu Sozeau2016-06-16
* | Not taking arguments given by name or position into account whenGravatar Hugo Herbelin2016-06-16
* | About printing of traces of failures while calling ltac code.Gravatar Hugo Herbelin2016-06-06
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-05-04
|\|
| * Fixing subst.out after changing spacing in goal output (24a125b77).Gravatar Hugo Herbelin2016-05-04
| * In Regular Subst Tactic mode, ensure that the order of hypotheses isGravatar Hugo Herbelin2016-05-03
| * Remove extraneous space in coqtop/pg output (bug #4675).Gravatar Guillaume Melquiond2016-05-03
* | Revert "A heuristic to add parentheses in the presence of rules such as"Gravatar Hugo Herbelin2016-04-27
* | A heuristic to add parentheses in the presence of rules such asGravatar Hugo Herbelin2016-04-27
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-04-24
|\|
| * Fixing output test Notations2.Gravatar Hugo Herbelin2016-04-22
| * Fixing #4677 (collision of a global variable and of a local variableGravatar Hugo Herbelin2016-04-19
* | A small test of Print Ltac.Gravatar Hugo Herbelin2016-04-09
* | Merge branch 'trunk-function_scope' of https://github.com/JasonGross/coq into...Gravatar Matthieu Sozeau2016-04-04
|\ \
* \ \ Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-02-13
|\ \ \ | | |/ | |/|
| * | Do not give a name to anonymous evars anymore. See bug #4547.Gravatar Pierre-Marie Pédrot2016-02-13
* | | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-12-17
|\| |
| * | Fix test suite after change in extraction.Gravatar Maxime Dénès2015-12-15
* | | Using x in output test-suite Cases.v (cosmetic).Gravatar Hugo Herbelin2015-12-05
* | | Fixing output test Cases.v.Gravatar Pierre-Marie Pédrot2015-11-15
* | | Updating test-suite after Bracketing Last Introduction Pattern set byGravatar Hugo Herbelin2015-11-10
* | | Merge origin/v8.5 into trunkGravatar Hugo Herbelin2015-11-10
|\| |
* | | Adapting output test inference.v after c23f0cab6 (experimentingGravatar Hugo Herbelin2015-11-08
| * | Fixing output test Existentials.v after eec77191b.Gravatar Hugo Herbelin2015-11-07
|/ /
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-26 06:51:14 +0000