aboutsummaryrefslogtreecommitdiff
path: root/test-suite/output
AgeCommit message (Expand)Author
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-07-12A short test on printing evars in Show Proof (this was wrong at some time).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
2015-07-27Output test for bug #2169.Pierre-Marie Pédrot
2015-06-24Fix test-suite after 1343b69221ce3eeb3154732e73bbdc0044b224a8.Maxime Dénès
2015-03-09Do not display the status of monomorphic constants unless in universe-polymor...Guillaume Melquiond
2015-03-05Fix testsuite with respect to the new formatting of Fail messages.Guillaume Melquiond
2015-02-15Undo: back to 8.4 semantics (Close #3514)Enrico Tassi
2015-01-12Fixing name of evars in output test Notation.v.Hugo Herbelin
2014-12-15Adapted test file for About.Pierre Courtieu
2014-12-15About now accepts hypothesis names and goal selector.Pierre Courtieu
2014-12-15Tests for Searchxxx commands added and modified.Pierre Courtieu
2014-11-11Adapting output tests to current naming of evars, even if unclearHugo Herbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-15 05:59:32 +0000