aboutsummaryrefslogtreecommitdiff
path: root/test-suite/output/Search.out
AgeCommit message (Expand)Author
2020-11-11Addressing #13349: accept Search on subparts of ident, not only on subidents.Hugo Herbelin
2020-11-06Merge PR #13255: Fixes #13244: support for coercions in Searchcoqbot-app[bot]
2020-11-04Typing patterns and using type constraints in Search.Hugo Herbelin
2020-10-30Renaming Numeral.v into Number.vPierre Roux
2020-07-08Adding test for #12525 (Search of lemmas in Include failing when in Module).Hugo Herbelin
2020-05-15Test new Search features.Théo Zimmermann
2020-05-15Cleaning the use of pstate and evar_map in Search.Hugo Herbelin
2020-05-15Search: Displaying the "use About" notice only when really needed.Hugo Herbelin
2020-05-09Add hexadecimal numeralsPierre Roux
2020-04-15[proof] Move functions related to `Proof.t` to `Proof`Emilio Jesus Gallego Arias
2020-03-18Change some ouput tests due to the printing of implicitsSimonBoulier
2019-03-14Inductives in SProp, forbid primitive records with only sprop fieldsGaëtan Gilbert
2018-11-28Byte.v: use right-associative tuples in bitsJason Gross
2018-11-28Speed up ByteJason Gross
2018-11-28Add `String Notation` vernacular like `Numeral Notation`Jason Gross
2017-04-21Remove VernacErrorGaetan Gilbert
2017-02-14Test-suite: output of SearchArnaud Spiwack
2014-12-15Tests for Searchxxx commands added and modified.Pierre Courtieu
2014-07-21Fixing output test-suite.Pierre-Marie Pédrot
2013-04-17Renaming SearchAbout into Search and Search into SearchHead.herbelin
2012-11-17Update output/Search.out after hint-related extra defs in Peanoletouzey
2011-05-16test-suite: no more ..._beq in the output of the search testsletouzey
2011-05-16Fix order in Search tests.letouzey
2011-05-06Fixes in the test-suite after modularisation of ZArith and coletouzey
2010-03-11Minimal test suite for search commandspuech
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 15:43:35 +0000