aboutsummaryrefslogtreecommitdiff
path: root/test-suite/output
AgeCommit message (Expand)Author
2016-07-19Some extra fixes in printing patterns in binders.Hugo Herbelin
2016-07-19Taking into account binding patterns when agglutinating sequences of binders.Hugo Herbelin
2016-07-19Fixing missing parentheses in printing of patterns in binders.Hugo Herbelin
2016-07-19Notations: fixing multiple binders used as terms in reverse order.Hugo Herbelin
2016-07-19Removing a source of clash with multiple recursive patterns in notations.Hugo Herbelin
2016-07-18A new step on using alpha-conversion in printing notations.Hugo Herbelin
2016-07-17Partial fix to #4592 (notation requiring alpha-conversion for printing).Hugo Herbelin
2016-07-17More examples of recursive notations, with emphasis in reference manual.Hugo Herbelin
2016-07-17Fixing a bug in recognizing a recursive pattern of notationsHugo Herbelin
2016-07-17Fixing interpretation of notations w/ opposite instances of a recursive pattern.Hugo Herbelin
2016-07-17Fixing printing of notations with several instances of a recursive pattern.Hugo Herbelin
2016-07-13Merge branch 'v8.5' into v8.6Pierre-Marie Pédrot
2016-07-13Fixing printing of evar name in an error message of instantiate.Hugo Herbelin
2016-06-29Fix issues in test-suite revealed by warnings.Maxime Dénès
2016-06-28Adding a test-suite for the only printing flag.Pierre-Marie Pédrot
2016-06-27Patterns in binders: printing testsArnaud Spiwack
2016-06-27Adding ability to put any pattern in binders, prefixed by a quote.Daniel de Rauglaudre
2016-06-24Fixing #4854 (regression introduced in 4d25b224 in relation with #4592).Hugo Herbelin
2016-06-18Exporting a generic argument induction_arg. As a consequence,Hugo Herbelin
2016-06-16proof mode: print unification constraintsMatthieu Sozeau
2016-06-16Not taking arguments given by name or position into account whenHugo Herbelin
2016-06-06About printing of traces of failures while calling ltac code.Hugo Herbelin
2016-05-04Merge branch 'v8.5'Pierre-Marie Pédrot
2016-05-04Fixing subst.out after changing spacing in goal output (24a125b77).Hugo Herbelin
2016-05-03In Regular Subst Tactic mode, ensure that the order of hypotheses isHugo Herbelin
2016-05-03Remove extraneous space in coqtop/pg output (bug #4675).Guillaume Melquiond
2016-04-27Revert "A heuristic to add parentheses in the presence of rules such as"Hugo Herbelin
2016-04-27A heuristic to add parentheses in the presence of rules such asHugo Herbelin
2016-04-24Merge branch 'v8.5'Pierre-Marie Pédrot
2016-04-22Fixing output test Notations2.Hugo Herbelin
2016-04-19Fixing #4677 (collision of a global variable and of a local variableHugo Herbelin
2016-04-09A small test of Print Ltac.Hugo Herbelin
2016-04-04Merge branch 'trunk-function_scope' of https://github.com/JasonGross/coq into...Matthieu Sozeau
2016-02-13Merge branch 'v8.5'Pierre-Marie Pédrot
2016-02-13Do not give a name to anonymous evars anymore. See bug #4547.Pierre-Marie Pédrot
2015-12-17Merge branch 'v8.5'Pierre-Marie Pédrot
2015-12-15Fix test suite after change in extraction.Maxime Dénès
2015-12-05Using x in output test-suite Cases.v (cosmetic).Hugo Herbelin
2015-11-15Fixing output test Cases.v.Pierre-Marie Pédrot
2015-11-10Updating test-suite after Bracketing Last Introduction Pattern set byHugo Herbelin
2015-11-10Merge origin/v8.5 into trunkHugo Herbelin
2015-11-08Adapting output test inference.v after c23f0cab6 (experimentingHugo Herbelin
2015-11-07Fixing output test Existentials.v after eec77191b.Hugo Herbelin
2015-10-22Fixing a bug in reporting ill-formed inductive.Hugo Herbelin
2015-10-11Fixing test-suiteHugo Herbelin
2015-10-11Fixing untimely unexpected warning "Collision between bound variables" (#4317).Hugo Herbelin
2015-10-11Refining 0c320e79ba30 in fixing interpretation of constr under bindersHugo Herbelin
2015-09-15Test for bug #4269.Pierre-Marie Pédrot
2015-09-03Update test-suite after 518049fe7.Maxime Dénès
2015-08-14Revert commit 18796b6aea453bdeef1ad12ce80eeb220bf01e67, close 3080Jason Gross
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-20 07:08:46 +0000