aboutsummaryrefslogtreecommitdiff
path: root/test-suite/output
AgeCommit message (Expand)Author
2020-11-27Merge PR #13473: Testing {in _, _} and {pred _} from ssrboolcoqbot-app[bot]
2020-11-25Testing {in _, _} and {pred _} from ssrboolCyril Cohen
2020-11-25Add tests for #13303Gaëtan Gilbert
2020-11-25Clean UnivBinders testGaëtan Gilbert
2020-11-24Merge PR #13436: Fixes #13432: typo in #11172 causing notations mentioning a ...coqbot-app[bot]
2020-11-22Adapting standard library, doc and test suite to ident->name renaming.Hugo Herbelin
2020-11-21Fixes #13432: regression with notations involving coercions caused by #11172.Hugo Herbelin
2020-11-20Tests for notations with general single (non-recursive) binders.Hugo Herbelin
2020-11-20Merge PR #12965: Fixes #9569: in notations with binders, prevent collisions b...coqbot-app[bot]
2020-11-19Merge PR #12984: [printing] Order notations by matching precision first, and ...coqbot-app[bot]
2020-11-18[attributes] Add output test suite for errors, improve error printing.Emilio Jesus Gallego Arias
2020-11-18In recursive notations, accept partial application over the recursive pattern.Hugo Herbelin
2020-11-17Merge PR #13390: Intern application arguments in left-to-right ordercoqbot-app[bot]
2020-11-17A reimport of notations now put the corresponding notations again in front.Hugo Herbelin
2020-11-17For printing, ordering notations by precision of the pattern.Hugo Herbelin
2020-11-16Merge PR #13384: Warn on hints without an explicit localitycoqbot-app[bot]
2020-11-16Fix #9569 (notations collect the spine binding variables at printing time).Hugo Herbelin
2020-11-16Merge PR #12690: Mini-fix of Locate for recursive notations using named varia...coqbot-app[bot]
2020-11-16Avoid exposing an internal names when "intros _ H" fails.Hugo Herbelin
2020-11-16Fix test-suite.Pierre-Marie Pédrot
2020-11-16Merge PR #13388: Export locality for all hint commandscoqbot-app[bot]
2020-11-15Intern application arguments in left-to-right orderGaëtan Gilbert
2020-11-15Ensuring the body of the notation in Locate is printed at level 0.Hugo Herbelin
2020-11-15Adding support for Locate "( x , y )".Hugo Herbelin
2020-11-15Fixing Locate for recursive notations with names.Hugo Herbelin
2020-11-15Merge PR #13376: Fixes #13266: Avoiding encapsulating exceptions w/o a handle...coqbot-app[bot]
2020-11-15Adding an output test to check that the hint commands respect their locality.Pierre-Marie Pédrot
2020-11-14Avoiding encapsulating exceptions w/o a handler in NotFoundInstance.Hugo Herbelin
2020-11-12Merge PR #13351: Fixes #13349: accept Search on subparts of an identifier, no...coqbot-app[bot]
2020-11-11Addressing #13349: accept Search on subparts of ident, not only on subidents.Hugo Herbelin
2020-11-09[obligation] Proper handle no obligations on `Next Obligation`Emilio Jesus Gallego Arias
2020-11-06Merge PR #13255: Fixes #13244: support for coercions in Searchcoqbot-app[bot]
2020-11-05Regression tests for the various combinations of mixed terms and binders in n...Hugo Herbelin
2020-11-05Merge PR #12218: Numeral notations for non inductive typescoqbot-app[bot]
2020-11-05Rename Dec and HexDec to Decimal and HexadecimalPierre Roux
2020-11-05Allow multiple primitive notation on the same scope and triggersPierre Roux
2020-11-05[string notation] Handle parameterized inductives and non inductivesPierre Roux
2020-11-05[numeral notation] Add support for parameterized inductivesPierre Roux
2020-11-05[numeral notation] Add tests for implicit argumentsPierre Roux
2020-11-05[numeral notation] RPierre Roux
2020-11-05[numeral notation] QPierre Roux
2020-11-04[numeral notation] Add tests for the via ... using ... optionPierre Roux
2020-11-04Typing patterns and using type constraints in Search.Hugo Herbelin
2020-11-04Fixes #13298: primitive projections needs a correct typing environment.Hugo Herbelin
2020-11-04Merge PR #13302: Fix test-suite in async mode.coqbot-app[bot]
2020-11-03Fix test-suite in async mode.Théo Zimmermann
2020-11-02Nicer spacing when printing array literalsGaëtan Gilbert
2020-11-02Merge PR #13247: Fixes #13241: nested Ltac functions wrongly reporting error ...Pierre-Marie Pédrot
2020-10-30Renaming Numeral.v into Number.vPierre Roux
2020-10-29Use same code for "Print Ltac foo" and "Print foo" when "foo" is an Ltac.Hugo Herbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-07-20 07:48:42 +0000