aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/output/SearchPattern.out
Commit message (Collapse)AuthorAge
* Update SearchPattern.out for numeral notationsGravatar Jason Gross2018-02-20
| | | | | | | | There is more churn than there should be because SearchPattern uses a non-local sorting algorithm; the comparison function considers many constants equal in priority and leaves it up to the heap structure to break ties, which seems wrong. This has been reported as [bug #5573](https://coq.inria.fr/bugs/show_bug.cgi?id=5573).
* Test-suite: output of SearchGravatar Arnaud Spiwack2017-02-14
| | | | | Fix the ordering of the results in the output of Search to correspond to the "priority" ordering.
* [search] Don't build intermediate lists in search.Gravatar Emilio Jesus Gallego Arias2016-10-20
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This patch converts the `search_*` functions to use an iter-style API. Consequently, the Search Vernac will produce a message for each search result, greatly improving roundtrip time as IDEs can effectively display the results in a streaming way. It also allows different printers to be used. I didn't observe a performance difference (as things seem to be dominated by printing and `Declaremods`). As a minor tweak, we make search with "Output Name Only" more efficient. Motivation: ----------- Currently, the main search API `Search.generic_search` is an effectful, iteration-based function: ```ocaml val generic_search : int option -> display_function -> unit ``` This type is imposed by `Declaremods`, which exposes an effectful, iteration-based API to traverse Coq library objects. The `Search.search_*` functions try to offer a more functional API by returning a list of pretty printing commands. They need to build an internal intermediate list for that purpose. However, this is a waste of time, as the destination of these lists is to be flushed out by the printer right away.
* Tests for Searchxxx commands added and modified.Gravatar Pierre Courtieu2014-12-15
|
* Consequence of changing the definition of Nat.shiftl and Nat.shiftr.Gravatar Hugo Herbelin2014-11-06
|
* Fixing output test-suite.Gravatar Pierre-Marie Pédrot2014-07-21
|
* Renaming SearchAbout into Search and Search into SearchHead.Gravatar herbelin2013-04-17
| | | | | | I hope I did not forget any place to change. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16423 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixing test-suite after last storm in Pp.Gravatar pboutill2012-06-12
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15433 85f007b7-540e-0410-9357-904b9bb8a0f7
* test-suite: no more ..._beq in the output of the search testsGravatar letouzey2011-05-16
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14128 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix order in Search tests.Gravatar letouzey2011-05-16
| | | | | | Signed-off-by: Tom Prince <tom.prince@ualberta.net> git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14127 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixes in the test-suite after modularisation of ZArith and coGravatar letouzey2011-05-06
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14114 85f007b7-540e-0410-9357-904b9bb8a0f7
* Minimal test suite for search commandsGravatar puech2010-03-11
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12860 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-28 11:41:21 +0000