aboutsummaryrefslogtreecommitdiff
path: root/test-suite/output
AgeCommit message (Expand)Author
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
2014-11-06Consequence of changing the definition of Nat.shiftl and Nat.shiftr.Hugo Herbelin
2014-10-23Fixing clash in output test-suite Cases.Hugo Herbelin
2014-10-23Taking into account factorization of consecutive names of same typesHugo Herbelin
2014-10-22Fixing typo in output test Notations.Hugo Herbelin
2014-10-21Adapting output tests to the removal of the new token warning and toHugo Herbelin
2014-10-20A patch for printing "match" when constructors are defined with let-inHugo Herbelin
2014-10-03Adapting output/Arguments_renaming continued.Hugo Herbelin
2014-10-02An evar name changed in output test.Hugo Herbelin
2014-10-02Adapting the output test Notations:Hugo Herbelin
2014-10-02Revert "test-suite: New names for vars but the expected invariant is preserved"Hugo Herbelin
2014-10-02Adapting output/Arguments_renaming.out after fixing printing ofHugo Herbelin
2014-09-27Adapting to naming of evars.Hugo Herbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-28 22:25:28 +0000